mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Basic
IsSelfAdjoint.nnnorm_mul_self : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E},
  IsSelfAdjoint x → ‖x * x‖₊ = ‖x‖₊ ^ 2
-- Mathlib.CategoryTheory.Sums.Associator
/-- Further characterizing the composition of the inverse of the associator and the right
inclusion.  -/
CategoryTheory.sum.inrCompInrCompInverseAssociator : (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] →
            (CategoryTheory.Sum.inr_ D E).comp
                ((CategoryTheory.Sum.inr_ C (D ⊕ E)).comp (CategoryTheory.sum.inverseAssociator C D E)) ≅
              CategoryTheory.Sum.inr_ (C ⊕ D) E
-- Init.Prelude
/-- A general error, given a message and a span (expressed as a `Syntax`).  -/
Lean.Macro.Exception.error : Lean.Syntax → String → Lean.Macro.Exception
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_eq_ofReal : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ₑ = ENNReal.ofReal r
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.continuous_toLower : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α],
  Continuous ⇑Topology.WithLower.toLower
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  -/
FiniteGrp.of : (G : Type u) → [Group G] → [Finite G] → FiniteGrp.{u}
-- Std.Do.Triple.SpecLemmas
List.Cursor.current_at : ∀ {α : Type u_1} {n : ℕ} (l : List α) (h : n < l.length), (List.Cursor.at l n).current ⋯ = l[n]
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaObject_left_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.mkCommaObject F).left.map f = F.map (CategoryTheory.WithTerminal.incl.map f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_containsKey : ∀ {α : Type u} {β : α → Type v} [instBEq : BEq α] [inst : Ord α] [Std.LawfulBEqOrd α] [Std.TransOrd α] {k : α}
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → Std.DTreeMap.Internal.Impl.contains k l = Std.Internal.List.containsKey k l.toListModel
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.deriv_norm_pos : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    0 < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofIntClamp n).toInt16 = Int16.ofInt n
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `f : {a : M // a ≠ 1} → α` function to `FiniteMulArchimedeanClass M → α`.  -/
FiniteMulArchimedeanClass.lift : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {α : Type u_2} →
          (f : { a // a ≠ 1 } → α) →
            (∀ (a b : { a // a ≠ 1 }),
                FiniteMulArchimedeanClass.mk ↑a ⋯ = FiniteMulArchimedeanClass.mk ↑b ⋯ → f a = f b) →
              FiniteMulArchimedeanClass M → α
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe : ∀ {n d : ℕ} (s : Fin (d + 1) ↪o Fin (n + 1)),
  ↑(SSet.stdSimplex.nonDegenerateEquiv.symm s) = SSet.stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk s.toOrderHom)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.snd.sizeOf_spec : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α₁] [inst_1 : SizeOf α₂]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (a : Std.IterM m β),
  sizeOf (Std.Iterators.Types.Append.snd a) = 1 + sizeOf a
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.isometry_comp : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃}
  {f : NormedAddGroupHom V₁ V₂}, Isometry ⇑g → Isometry ⇑f → Isometry ⇑(g.comp f)
-- Batteries.Data.Fin.Coding
Fin.encodeOption_decodeOption : ∀ {n : ℕ} (x : Fin (n + 1)), Fin.encodeOption (Fin.decodeOption x) = x
-- Lean.Meta.Match.Basic
/-- Return `true` if `fvarId` is one of the alternative pattern variables  -/
Lean.Meta.Match.Alt.isLocalDecl : Lean.FVarId → Lean.Meta.Match.Alt → Bool
-- Mathlib.Algebra.Module.PUnit
PUnit.smul_eq : ∀ {R : Type u_3} (y : PUnit.{u_4 + 1}) (r : R), r • y = PUnit.unit
-- Mathlib.Topology.Baire.Lemmas
/-- A dense Gδ subset of a Baire space is Baire.  -/
IsGδ.baireSpace_of_dense : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, IsGδ s → Dense s → BaireSpace ↑s
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).CorootForm = (killingForm K L).restrict H.toSubmodule
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.add_sSup : ∀ (o : Ordinal.{u}) {s : Set Ordinal.{u}} [Small.{u, u + 1} ↑s], s.Nonempty → o + sSup s = sSup ((fun x => o + x) '' s)
-- Mathlib.Control.ULift
PLift.pure.eq_1 : ∀ {α : Sort u}, PLift.pure = PLift.up
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_eq_biInter_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E}, tangentConeAt 𝕜 s x = ⋂ U ∈ nhds 0, closure (Set.univ • (U ∩ (fun x_1 => x + x_1) ⁻¹' s))
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceComposableArrows₅.eq_1 : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  F.homologySequenceComposableArrows₅ T n₀ n₁ h =
    CategoryTheory.ComposableArrows.mk₅ ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂)
      (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ((F.shift n₁).map T.mor₂)
-- Mathlib.Topology.UniformSpace.Closeds
isTrans_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) [U.IsTrans], (hausdorffEntourage U).IsTrans
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instMin : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → Min (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.ediam_range : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → Metric.ediam (Set.range f) = Metric.ediam Set.univ
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.colLen.eq_1 : ∀ (μ : YoungDiagram) (j : ℕ), μ.colLen j = Nat.find ⋯
-- Mathlib.CategoryTheory.Yoneda
/-- The "Yoneda pairing" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `yoneda.op.obj X ⟶ F`, functorially in both `X` and `F`.
 -/
CategoryTheory.yonedaPairing : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_left : ∀ {x y : ℝ}, 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_sum : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : MeasureTheory.SimpleFunc α ENNReal)
  (μ : ι → MeasureTheory.Measure α), f.lintegral (MeasureTheory.Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.inter m₂).get? k = if m₂.contains k = true then m₁.get? k else none
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.IsNilRegular.eq_1 : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] (x : L),
  φ.IsNilRegular x = ((LinearMap.charpoly (φ x)).coeff φ.nilRank ≠ 0)
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft.eq_1 : ∀ (a b : ℕ),
  a.factorizationLCMLeft b =
    (a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1
-- Mathlib.Data.Sum.Order
OrderIso.sumDualDistrib_symm_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (b : β),
  (OrderIso.sumDualDistrib α β).symm (Sum.inr (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) (s : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h (CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s) = s
-- Mathlib.Data.List.Sublists
List.sublistsLenAux.eq_def : ∀ {α : Type u} {β : Type v} (x : ℕ) (x_1 : List α) (x_2 : List α → β) (x_3 : List β),
  List.sublistsLenAux x x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | 0, x, f, r => f [] :: r
    | n.succ, [], x, r => r
    | n.succ, a :: l, f, r => List.sublistsLenAux (n + 1) l f (List.sublistsLenAux n l (f ∘ List.cons a) r)
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.toLinearMap_comp : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {N : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R N] {Q₁ : QuadraticMap R M₁ N}
  {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂),
  (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The middle right map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePre' F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePost F)
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`.  -/
Finset.prod_powerset_insert : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : CommMonoid β] [inst_1 : DecidableEq α],
  a ∉ s →
    ∀ (f : Finset α → β), ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)
-- Lean.CoreM
/-- Cache of `Lean.inheritedTraceOptions`.  -/
Lean.Core.Context.inheritedTraceOptions : Lean.Core.Context → Std.HashSet Lean.Name
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_nonempty : ∀ {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] {s : Set X}, ((Convexity.convexHull R) s).Nonempty ↔ s.Nonempty
-- Init.Data.List.Nat.Erase
List.set_eraseIdx_gt : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} {a : α}, j < i → (xs.eraseIdx i).set j a = (xs.set j a).eraseIdx i
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.commRing : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → CommRing (R ⧸ I)
-- Lean.Elab.Quotation
/-- Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern).  -/
Lean.Elab.Term.Quotation.MatchResult : Type
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.isNilpotent_iff_charpoly : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Finite R M] [inst_5 : Module.Free R M] (φ : Module.End R M),
  IsNilpotent φ ↔ LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fap.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fn : Lean.Name) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13),
  sizeOf (Lean.Compiler.LCNF.LetValue.fap fn args h) = 1 + sizeOf fn + sizeOf args + sizeOf h
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- **Alias** of `Matroid.eRk_inter_add_eRk_union_le`.

---

The `ℕ∞`-valued rank function is submodular.  -/
Matroid.eRk_submod : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.eq_formallyUnramified_and_smooth : @RingHom.Etale = fun R S x x_1 f => f.FormallyUnramified ∧ f.Smooth
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pointwise_smul_toSubmonoid : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (a : α)
  (S : Subgroup G), (a • S).toSubmonoid = a • S.toSubmonoid
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instFiniteCarrierToGrp : ∀ (G : FiniteGrp.{u_1}), Finite ↑G.toGrp
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_le_of_edist_le : ∀ {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞}, (∀ (u v : α), G.edist u v ≤ k) → G.ediam ≤ k
-- Mathlib.RingTheory.Ideal.Maps
Ideal.IsMaximal.comap_piEvalRingHom : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] {i : ι} {I : Ideal (R i)},
  I.IsMaximal → (Ideal.comap (Pi.evalRingHom R i) I).IsMaximal
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_τ₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH2 f φ).τ₁ = groupHomology.chainsMap₃ f φ
-- Mathlib.Topology.Algebra.Indicator
Continuous.indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : Zero β], (∀ a ∈ frontier s, f a = 0) → Continuous f → Continuous (s.indicator f)
-- Mathlib.NumberTheory.PythagoreanTriples
/-- By assuming `x` is odd and `z` is positive we get a slightly more precise classification of
the Pythagorean triple `x ^ 2 + y ^ 2 = z ^ 2`.  -/
PythagoreanTriple.coprime_classification' : ∀ {x y z : ℤ},
  PythagoreanTriple x y z →
    x.gcd y = 1 →
      x % 2 = 1 →
        0 < z →
          ∃ m n,
            x = m ^ 2 - n ^ 2 ∧
              y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLT_eq_posLE : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p}, s.posLT p h = s.posLE p.dec
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp X.hom (T.map (CategoryTheory.StructuredArrow.Hom.right f)) = Y.hom
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_sup : ∀ {α : Type u_1} [inst : LE α] (s t : LowerSet α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Init.Data.Float.Model.Unpacked.Operations.Add
/-- Computes the sum of two floating point numbers and rounds the result according to
the given specification.
 -/
Float.Model.UnpackedFloat.add : Float.Model.Format → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_partialSups : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {ι : Type u_1} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι]
  {s : ι → Set α}, (∀ (i : ι), m.IsCaratheodory (s i)) → ∀ (i : ι), m.IsCaratheodory ((partialSups s) i)
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_neg : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G],
  Isometry Neg.neg
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_add_of_nonneg : ∀ {x : ENNReal} (y z : ℝ), 0 ≤ y → 0 ≤ z → x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Integrate `f(x₁,…,xₙ)` over all variables `xᵢ` where `i ∈ s`. Return a function in the
remaining variables (it will be constant in the `xᵢ` for `i ∈ s`).
This is the marginal distribution of all variables not in `s` when the considered measure
is the product measure.  -/
MeasureTheory.«term∫⋯∫⁻__,_∂_» : Lean.ParserDescr
-- Mathlib.Data.Set.Finite.Basic
Set.card_range_of_injective : ∀ {α : Type u} {β : Type v} [inst : Fintype α] {f : α → β},
  Function.Injective f → ∀ [inst_1 : Fintype ↑(Set.range f)], Fintype.card ↑(Set.range f) = Fintype.card α
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_contract' : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) [ExpChar R p] [NoZeroDivisors R] {f : Polynomial R},
  Polynomial.derivative f = 0 → (Polynomial.expand R p) (Polynomial.contract p f) = f
-- Mathlib.Tactic.TermCongr
/-- A congruence lemma between two expressions. The proof is generated dynamically, depending on
whether the resulting lemma should be an `Eq` or a `HEq`.
If generating a proof impossible, then the generator can throw an error.
This can be due to either an `Eq` proof being impossible
or due to the lhs/rhs not being defeq to the lhs/rhs of the generated proof,
which can happen for user-supplied congruence holes.

This complexity is to support two features:

1. The user is free to supply Iff, Eq, and HEq lemmas in congruence holes,
   and we're able to transform them into whatever is appropriate for a
   given congruence lemma.
2. If the congruence hole is a metavariable, then we can specialize that
   hole to an Iff, Eq, or HEq depending on what's necessary at that site.  -/
Mathlib.Tactic.TermCongr.CongrResult : Type
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- A variant of `exact_liftBaseChange_map_of_flat` that takes in
arbitrary maps between generators.  -/
Algebra.Generators.H1Cotangent.exact_liftBaseChange_map_of_flat' : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} {τ : Type w₅} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (W : Algebra.Generators R T τ) [Module.Flat S T] (f : W.Hom Q) (g : P.Hom W),
  Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.H1Cotangent.map g.toExtensionHom))
    ⇑(Algebra.Extension.H1Cotangent.map f.toExtensionHom)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add f) CategoryTheory.AddMonObj.add) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f)
          CategoryTheory.AddMonObj.add))
      CategoryTheory.AddMonObj.add
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.eq_def : ∀ (rhsRoot lhsRoot : Lean.Meta.Grind.ENode) (rhsTerms lhsTerms : Lean.Meta.Grind.SolverTerms),
  Lean.Meta.Grind.Solvers.mergeTerms.go✝ rhsRoot lhsRoot rhsTerms lhsTerms =
    match rhsTerms, lhsTerms with
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil =>
      pure (Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.PendingSolverPropagationsData.nil✝)
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest => do
      let __do_lift ← Lean.Meta.Grind.getParents rhsRoot.self
      pure (lhsTerms, Lean.Meta.Grind.Solvers.mergeTerms.toPendingDiseqs✝ lhsTerms __do_lift)
    | Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil => do
      let __do_lift ← Lean.Meta.Grind.getParents lhsRoot.self
      pure (rhsTerms, Lean.Meta.Grind.Solvers.mergeTerms.toPendingDiseqs✝ rhsTerms __do_lift)
    | Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms =>
      if (id₁ == id₂) = true then do
        let __x ← Lean.Meta.Grind.Solvers.mergeTerms.go✝ rhsRoot lhsRoot rhsTerms lhsTerms
        match __x with
          | (s, p) =>
            pure
              (Lean.Meta.Grind.SolverTerms.next id₁ rhs s,
                Lean.Meta.Grind.PendingSolverPropagationsData.eq✝ id₁ lhs rhs p)
      else
        if id₁ < id₂ then do
          let __x ←
            Lean.Meta.Grind.Solvers.mergeTerms.go✝ rhsRoot lhsRoot rhsTerms
                (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)
          match __x with
            | (s, p) => do
              let __do_lift ← Lean.Meta.Grind.getParents lhsRoot.self
              pure
                  (Lean.Meta.Grind.SolverTerms.next id₁ rhs s,
                    Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ id₁ __do_lift p)
        else do
          let __x ←
            Lean.Meta.Grind.Solvers.mergeTerms.go✝ rhsRoot lhsRoot (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                lhsTerms
          match __x with
            | (s, p) => do
              let __do_lift ← Lean.Meta.Grind.getParents rhsRoot.self
              pure
                  (Lean.Meta.Grind.SolverTerms.next id₂ lhs s,
                    Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ id₂ __do_lift p)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome).get!