mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Basic
Representation.asAlgebraHom_single_one : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G), ρ.asAlgebraHom (MonoidAlgebra.single g 1) = ρ g
-- Std.Data.HashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.Raw.getKey! : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [Inhabited α] → Std.HashMap.Raw α β → α → α
-- Lean.Meta.IndPredBelow
/-- Replaces the application of the motive with the corresponding below name.
Example:
```
(a : Nat) → motive (f a)
==>
(a : Nat) → ABC.below (f a)
```
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.ihTypeToBelowType : Lean.Expr → Lean.Meta.IndPredBelow.Context✝ → Lean.Expr
-- Init.Data.String.Basic
String.Slice.Pos.prevAux : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.startPos → String.Pos.Raw
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Version of `mlieBracketWithin_congr` in which one assumes that the point belongs to the
given set.  -/
VectorField.mlieBracketWithin_congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  Set.EqOn V₁ V s →
    Set.EqOn W₁ W s → x ∈ s → VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatch_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch p pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true
-- Mathlib.Order.Monotone.Monovary
StrictMono.trans_antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : PartialOrder ι], StrictMono f → Antivary g f → Antitone g
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.auxTransvection.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] {e : V ≃ₗ[K] V}
  {f : Module.Dual K V} {u : V} (hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f),
  LinearEquiv.auxTransvection✝ hf = LinearEquiv.transvection ⋯
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_tsum : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace E] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7}
  [Countable ι] {f : ι → α → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ⊤ →
      (MeasureTheory.setToFun μ T hT fun a => ∑' (i : ι), f i a) = ∑' (i : ι), MeasureTheory.setToFun μ T hT (f i)
-- Mathlib.Data.Set.Prod
/-- The fiber product $X \times_Y Z$.  -/
Function.Pullback : {X : Type u_1} → {Y : Sort u_2} → {Z : Type u_3} → (X → Y) → (Z → Y) → Type (max 0 u_3 u_1)
-- Mathlib.RingTheory.WittVector.Basic
/-- `WittVector.ghostMap` is a ring isomorphism when `p` is invertible in `R`.  -/
WittVector.ghostEquiv : (p : ℕ) →
  (R : Type u_1) → [inst : CommRing R] → [inst_1 : Fact (Nat.Prime p)] → [Invertible ↑p] → WittVector p R ≃+* (ℕ → R)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.forget_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C)
  {X Y : CategoryTheory.Endofunctor.Algebra F} (self : X.Hom Y),
  (CategoryTheory.Endofunctor.Algebra.forget F).map self = self.f
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- `AEEqFun.toGerm` as a `MonoidHom`.  -/
MeasureTheory.AEEqFun.toGermMonoidHom : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : Monoid γ] → [inst_3 : ContinuousMul γ] → (α →ₘ[μ] γ) →* (MeasureTheory.ae μ).Germ γ
-- Lean.Parser.Term
Lean.Parser.Term.argument.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_rpow_inv_iff_of_pos : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {t : Std.DTreeMap.Internal.Impl α β},
  t.Balanced →
    t.Ordered →
      (Std.DTreeMap.Internal.Impl.containsThenInsert! k v t).2.toListModel.Perm
        (Std.Internal.List.insertEntry k v t.toListModel)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote : Nat.Internal.Linear.Context → Nat.Internal.Linear.Poly → ℕ
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex.X₁ = X₁
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- **Alias** of `Measurable.infEDist`. -/
Measurable.infEdist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → ∀ {s : Set α}, Measurable fun x => Metric.infEDist (f x) s
-- Mathlib.Order.Filter.Map
Filter.bot_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, ⊥ = Filter.map m f ↔ f = ⊥
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], NonemptyInterval.toProd 0 = 0
-- Batteries.Tactic.PrintOpaques
/-- The collected opaque defs.  -/
Batteries.Tactic.CollectOpaques.State.opaques : Batteries.Tactic.CollectOpaques.State → Array Lean.Name
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context.mk.injEq : ∀ (steps steps_1 : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step)),
  ({ steps := steps } = { steps := steps_1 }) = (steps = steps_1)
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.coneOfLowerBound_π_app : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)) (i : J),
  (Preorder.coneOfLowerBound F h).π.app i = CategoryTheory.homOfLE ⋯
-- Mathlib.RingTheory.Coalgebra.Convolution
Coalgebra.Repr.convMul_apply : ∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} {ι : Type u_6} [inst : CommSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A]
  [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C] {a : C}
  (𝓡 : Coalgebra.Repr R a ι) (f g : WithConv (C →ₗ[R] A)),
  (f * g).ofConv a = ∑ i ∈ 𝓡.index, f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
/-- Given `P : ObjectProperty C`, we say that `P.ContainsZero` if there exists
a zero object for which `P` holds. When `P` is closed under isomorphisms,
this holds for any zero object.  -/
CategoryTheory.ObjectProperty.ContainsZero : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor α).inv.τl = (CategoryTheory.Bicategory.rightUnitor α.l).inv
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of an operator from the finite-dimensional inner product space `E` to the
finite-dimensional inner product space `F`.  -/
LinearMap.adjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : InnerProductSpace 𝕜 E] →
              [inst_4 : InnerProductSpace 𝕜 F] →
                [FiniteDimensional 𝕜 E] → [FiniteDimensional 𝕜 F] → (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isZero : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Bool
-- Init.Data.Vector.Count
Vector.one_le_countP_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, 1 ≤ Vector.countP p xs ↔ ∃ a ∈ xs, p a = true
-- Mathlib.Topology.Irreducible
/-- The set of irreducible components of a topological space.  -/
irreducibleComponents : (X : Type u_3) → [TopologicalSpace X] → Set (Set X)
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_singleton : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] (i : ι)
  {w : ι → R} (z : ι → E), w i ≠ 0 → {i}.centerMass w z = z i
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- Converting a commutative monoid object in `Type` to a bundled commutative monoid.
 -/
CommMonTypeEquivalenceCommMon.functor : CategoryTheory.Functor (CategoryTheory.CommMon (Type u)) CommMonCat
-- Mathlib.Data.Stream.Init
Stream'.iterate.eq_1 : ∀ {α : Type u} (f : α → α) (a : α), Stream'.iterate f a 0 = a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.colimit_ι_zero_cokernel_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.CategoryStruct.comp f g = 0)
  [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f 0)
        CategoryTheory.Limits.WalkingParallelPair.zero)
      (CategoryTheory.Limits.cokernel.desc f g h) =
    0
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.IsLinear.mk : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  {e : Bundle.Trivialization F Bundle.TotalSpace.proj},
  (∀ b ∈ e.baseSet, IsLinearMap R fun x => (↑e ⟨b, x⟩).2) → Bundle.Trivialization.IsLinear R e
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.IsProbabilityMeasure μ ↔ μ Set.univ = 1
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.continuous_polynomial_eval_inv_mul : ∀ (p : Polynomial ℝ), Continuous fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The right homotopy relation is transitive.
 -/
SSet.Truncated.HomotopicR.trans : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g h : SSet.Truncated.Edge x y},
  SSet.Truncated.HomotopicR f g → SSet.Truncated.HomotopicR g h → SSet.Truncated.HomotopicR f h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofList_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {k : α} {v : β k}
  {tl : List ((a : α) × β a)}, Std.DHashMap.Raw.ofList (⟨k, v⟩ :: tl) = (∅.insert k v).insertMany tl
-- Init.Data.BitVec.Lemmas
BitVec.not_self_ne : ∀ {w : ℕ} {a : BitVec w}, 0 < w → ~~~a ≠ a
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_subRight : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd G] (g : G),
  MeasurableEmbedding fun x => x - g
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Free.eq_1 : ∀ {α : Type u_4} {β : Type u_5} (A : SimpleGraph α) (B : SimpleGraph β), A.Free B = ¬A.IsContained B
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The chosen coequalizer of a parallel pair is a regular epimorphism.  -/
CategoryTheory.coequalizerRegular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (g h : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair g h)] →
          CategoryTheory.RegularEpi (CategoryTheory.Limits.coequalizer.π g h)
-- Mathlib.Data.List.Cycle
Cycle.nodup_nil : ∀ {α : Type u_1}, Cycle.nil.Nodup
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).get k h' = t.get k ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The change of variables mapped over a ring homomorphism `φ : R →+* A`.  -/
WeierstrassCurve.VariableChange.map : {R : Type u} →
  [inst : CommRing R] →
    WeierstrassCurve.VariableChange R →
      {A : Type v} → [inst_1 : CommRing A] → (R →+* A) → WeierstrassCurve.VariableChange A
-- Mathlib.Topology.Algebra.Monoid
continuousOn_multiset_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).prod) t
-- Mathlib.Topology.FiberBundle.Basic
/-- The projection on the base of a fiber bundle created from core is continuous  -/
FiberBundleCore.continuous_proj : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F), Continuous Z.proj
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isPrimitiveClassified_aux : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z),
  x.gcd y = 1 →
    0 < z →
      ∀ {m n : ℤ},
        0 < m ^ 2 + n ^ 2 →
          ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2) →
            ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2) →
              (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1 →
                m.gcd n = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0 → h.IsPrimitiveClassified
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- If `f₀` is homotopic to `f₁` relative to a pre-path object `P`,
and `f₁` is homotopic to `f₂` relative to `P'`, then
`f₀` is homotopic to `f₂` relative to `P.trans P'`.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      {P : HomotopicalAlgebra.PrepathObject Y} →
        {X : C} →
          {f₀ f₁ f₂ : X ⟶ Y} →
            P.RightHomotopy f₀ f₁ →
              {P' : HomotopicalAlgebra.PrepathObject Y} →
                P'.RightHomotopy f₁ f₂ →
                  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] → (P.trans P').RightHomotopy f₀ f₂
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- `homogeneousComponent n φ` is the part of `φ` that is homogeneous of degree `n`.
See `sum_homogeneousComponent` for the statement that `φ` is equal to the sum
of all its homogeneous components.  -/
MvPolynomial.homogeneousComponent : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → ℕ → MvPolynomial σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.coconePointSMul_apply : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] (r : R),
  (ModuleCat.HasColimit.coconePointSMul F) r =
    CategoryTheory.Limits.colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.declValToTerm : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le' : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : Zero M] {s : Set α} {f g : α → M},
  (∀ a ∈ s, f a ≤ g a) → (∀ a ∉ s, 0 ≤ g a) → s.indicator f ≤ g
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.filter_pairs_lt : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] (k : ℕ),
  {x ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k |
      match x with
      | (s, snd) => s.card < k} =
    (Finset.range k).disjiUnion (fun x => Finset.powersetCard x Finset.univ) ⋯ ×ˢ Finset.univ
-- Mathlib.Geometry.Convex.Hull
/-- **Alias** of the reverse direction of `Convexity.convexHull_eq_self`. -/
Convexity.IsConvexSet.convexHull_eq_self : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {C : Set X}, Convexity.IsConvexSet R C → (Convexity.convexHull R) C = C
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- A `EuclideanDomain` is a non-trivial commutative ring with a division and a remainder,
satisfying `b * (a / b) + a % b = a`.
The definition of a Euclidean domain usually includes a valuation function `R → ℕ`.
This definition is slightly generalised to include a well-founded relation
`r` with the property that `r (a % b) b`, instead of a valuation.  -/
EuclideanDomain : Type u → Type u
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIsTorsionFree : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] [inst_2 : Module S R]
  [Module.IsTorsionFree S R], Module.IsTorsionFree S (Polynomial R)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸},
  DifferentiableAt 𝕜 c x → ∀ (d : 𝔸), deriv (fun y => c y * d) x = deriv c x * d
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the reverse direction of `ContinuousLinearMapWOT.continuousAt_iff`. -/
ContinuousLinearMapWOT.continuousAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α},
  (∀ (x : E) (y : F), ContinuousAt (fun x_1 => inner 𝕜 y ((f x_1) x)) a) → ContinuousAt f a
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_apply_left : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} (u : ↥p), (LinearMap.ofIsCompl h φ ψ) ↑u = φ u
-- Mathlib.Order.Monotone.Defs
strictMonoOn_id : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, StrictMonoOn id s
-- Init.Data.Int.Order
Int.sign_eq_one_of_pos : ∀ {a : ℤ}, 0 < a → a.sign = 1
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The additive `p`-adic valuation on `ℚ_[p]`, with values in `WithTop ℤ`.  -/
Padic.addValuationDef : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℚ_[p] → WithTop ℤ
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- The left ideal of matrices with entries in `I ≤ R`.  -/
Ideal.matrix : {R : Type u_1} →
  [inst : Semiring R] →
    (n : Type u_2) → [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Ideal R → Ideal (Matrix n n R)
-- Mathlib.Probability.Independence.Basic
/-- Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`.
We use the notation `f ⟂ᵢ[μ] g` for `IndepFun f g μ` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.«term_⟂ᵢ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Order.RelSeries
SetRel.infiniteDimensional_inv : ∀ {α : Type u_1} {r : SetRel α α}, r.inv.InfiniteDimensional ↔ r.InfiniteDimensional
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology functor `ShortComplex C ⥤ C`, where the right homology of a
short complex `S` is understood as a kernel of the obvious map `S.fromOpcycles : S.opcycles ⟶ S.X₃`
where `S.opcycles` is a cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.rightHomologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.Topology.Order.LeftRight
nhdsWithinGT_sup_nhdsWithinLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Ioi a) ⊔ nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a (s \ {a})
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_sInf : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : Set (AddSubmonoid M)), (sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.csSup_lt_iff : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {a : α},
  s.Finite → s.Nonempty → (sSup s < a ↔ ∀ x ∈ s, x < a)
-- Init.Data.Prod
Prod.swap_swap_eq : ∀ {α : Type u_1} {β : Type u_2}, Prod.swap ∘ Prod.swap = id
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderiv_continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} [inst_7 : Fintype ι],
  DifferentiableAt 𝕜 c x → ∀ (u : (i : ι) → M i), fderiv 𝕜 (fun y => (c y) u) x = (fderiv 𝕜 c x).flipMultilinear u
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk_add : ∀ {M : Type u_1} [inst : Add M] (a b : M), DomAddAct.mk (a + b) = DomAddAct.mk b + DomAddAct.mk a
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNatLT : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatLT n hn).toUInt8 = UInt8.ofNat n
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- Pull a subring back to an opposite subring along `MulOpposite.unop`  -/
Subring.op : {R : Type u_2} → [inst : NonAssocRing R] → Subring R → Subring Rᵐᵒᵖ
-- Lean.MetavarContext
/-- Modify the local context of a metavariable. If the metavariable is not declared,
the `MetavarContext` is returned unchanged.

You must ensure that the modification is legal. In particular, expressions may
only be replaced with defeq expressions.
 -/
Lean.MetavarContext.modifyExprMVarLCtx : Lean.MetavarContext → Lean.MVarId → (Lean.LocalContext → Lean.LocalContext) → Lean.MetavarContext