mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (i : Y.I)
  (f : X ⟶ Y.obj i) (x : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I),
  (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i f).φ x = f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K] (r : S)
  (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)),
  { toCompletion := ↑(r • x) } = r • { toCompletion := ↑x }
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.vsub_linear : ∀ {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] (f g : P1 →ᵃ[k] P2), (f -ᵥ g).linear = f.linear - g.linear
-- Mathlib.RingTheory.Ideal.Operations
/-- An ideal is radical if it contains its radical.  -/
Ideal.IsRadical : {R : Type u} → [inst : CommSemiring R] → Ideal R → Prop
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_pure : ∀ {α : Type u_1} (a : α), (pure a).IsCountablyGenerated
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csInf_Ici : ∀ {α : Type u_5} [inst : ConditionallyCompletePartialOrderInf α] {a : α}, sInf (Set.Ici a) = a
-- Init.Data.SInt.Bitwise
Int16.and_eq_neg_one_iff : ∀ {a b : Int16}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound.injEq : ∀ (h h_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound h = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound h_1) = (h = h_1)
-- Mathlib.Topology.Order.LiminfLimsup
/-- A continuous monotone function between (conditionally) complete linear ordered spaces sends a
`Filter.liminf` to the `Filter.liminf` of the images (if the filter is bounded from below and
frequently bounded from above).  -/
Monotone.map_liminf_of_continuousAt : ∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder R]
  [inst_1 : TopologicalSpace R] [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S]
  [inst_4 : TopologicalSpace S] [OrderTopology S] {f : R → S},
  Monotone f →
    ∀ (a : ι → R),
      ContinuousAt f (Filter.liminf a F) →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F a) Monotone.map_liminf_of_continuousAt._auto_1 →
          autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F a) Monotone.map_liminf_of_continuousAt._auto_3 →
            f (Filter.liminf a F) = Filter.liminf (f ∘ a) F
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_op : ∀ {G : Type u_2} [inst : AddGroup G] (S : AddSubgroup G), S.op.unop = S
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.instZeroHomComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) → [R.Additive] → {u v : CategoryTheory.Comma L R} → Zero (u ⟶ v)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- The path component of the identity in the unitary group of a C⋆-algebra is the set of
unitaries that can be expressed as a product of exponential unitaries.  -/
Unitary.mem_pathComponentOne_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : ↥(unitary A)},
  u ∈ pathComponent 1 ↔ ∃ l, (List.map selfAdjoint.expUnitary l).prod = u
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- An excenter of a triangle bisects the angle at a vertex modulo `π`.  -/
Affine.Triangle.two_zsmul_oangle_excenter_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ (signs : Finset (Fin 3)),
          2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t signs) =
            2 • EuclideanGeometry.oangle (Affine.Simplex.excenter t signs) (t.points i₁) (t.points i₃)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier : Set α) (isClosed' : IsClosed carrier) (carrier_1 : Set α)
  (isClosed'_1 : IsClosed carrier_1),
  ({ carrier := carrier, isClosed' := isClosed' } = { carrier := carrier_1, isClosed' := isClosed'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_two_pi : ∀ (x : ℝ), Real.sin (x - 2 * Real.pi) = Real.sin x
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- A cone `c` on `F : J ⥤ C` lifts to a cone in `Over c.pt` with cone point `𝟙 c.pt`.  -/
CategoryTheory.Limits.Cone.toUnder : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            CategoryTheory.Limits.Cone (c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.toUnder c.pt F))
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A fixed block is an invariant block.  -/
MulAction.IsFixedBlock.isInvariantBlock : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsFixedBlock G B → MulAction.IsInvariantBlock G B
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.countPBefore.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (i s : ℕ)
  (h_1 : (head : α) → (tail : List α) → (s : ℕ) → motive (head :: tail) 0 s)
  (h_2 : (a : α) → (xs : List α) → (i s : ℕ) → motive (a :: xs) i.succ s) (h_3 : (x s : ℕ) → motive [] x s),
  (match a :: xs, i.succ, s with
    | head :: tail, 0, s => h_1 head tail s
    | a :: xs, i.succ, s => h_2 a xs i s
    | [], x, s => h_3 x s) =
    h_2 a xs i s
-- Mathlib.Data.Real.Embedding
Archimedean.embedReal_injective : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : One M]
  [inst_4 : ZeroLEOneClass M] [inst_5 : NeZero 1] [inst_6 : Archimedean M],
  Function.Injective ⇑(Archimedean.embedReal M)
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec_eq : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.ushiftRightRec y n = x >>> BitVec.setWidth w₂ (BitVec.setWidth (n + 1) y)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isGLB_neg' : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsGLB (-s) (-a) ↔ IsLUB s a
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `lift` with `Z` a terminal object.  -/
CategoryTheory.WithTerminal.liftToTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          CategoryTheory.Functor C D →
            CategoryTheory.Limits.IsTerminal Z → CategoryTheory.Functor (CategoryTheory.WithTerminal C) D
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consEntries.inj : ∀ {α : Type u} {β : Type v} {a : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))}
  {a_1 : Lean.PersistentHashMap.Zipper α β}
  {a_2 : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))}
  {a_3 : Lean.PersistentHashMap.Zipper α β},
  Lean.PersistentHashMap.Zipper.consEntries a a_1 = Lean.PersistentHashMap.Zipper.consEntries a_2 a_3 →
    a = a_2 ∧ a_1 = a_3
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_add_minimalPeriod_eq : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, f^[n + Function.minimalPeriod f x] x = f^[n] x
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAtChain_startPos_endPos_iff_toList : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestMatchAtChain c s.startPos s.endPos ↔
    s.copy.toList = List.replicate s.copy.toList.length c
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntryIfNew_le_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) {km kmi : α},
  Std.Internal.List.minKey? l = some km →
    (Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi → (compare kmi km).isLE = true
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.smul_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [TrivialStar R] [inst_2 : AddCommGroup A] [inst_3 : StarAddMonoid A]
  [inst_4 : Monoid R] [inst_5 : DistribMulAction R A] [StarModule R A] (r : R) {x : A},
  x ∈ skewAdjoint A → r • x ∈ skewAdjoint A
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_tan : ∀ (x : ℝ), ↑(Real.tan x) = Complex.tan ↑x
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.maximalIdeal.congr_simp : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A],
  IsDiscreteValuationRing.maximalIdeal A = IsDiscreteValuationRing.maximalIdeal A
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instSDiff : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → SDiff (L.DefinableSet A α)
-- Lean.KeyedDeclsAttribute
_private.Lean.KeyedDeclsAttribute.0.Lean.KeyedDeclsAttribute.Table.insert : {γ : Type} →
  Lean.KeyedDeclsAttribute.Table γ → Lean.KeyedDeclsAttribute.AttributeEntry γ → Lean.KeyedDeclsAttribute.Table γ
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.F₄_det : CartanMatrix.F₄.det = 1
-- Mathlib.Topology.Continuous
/-- See also `interior_preimage_subset_preimage_interior`.  -/
preimage_interior_subset_interior_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y},
  Continuous f → f ⁻¹' interior t ⊆ interior (f ⁻¹' t)
-- Std.Do.PostCond
/-- Entailment of exception assertions is defined as pointwise entailment of the assertions for each
potential exception.

While implication of exception conditions (`ExceptConds.imp`) is itself an exception condition,
entailment is an ordinary proposition.
 -/
Std.Do.«term_⊢ₑ_» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_ind : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  {motive : Std.DHashMap.Raw α β → Prop} (m : Std.DHashMap.Raw α β) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Raw α β) (a : α) (b : β a), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = false → t.getKey? a = none
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.eq_1 : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] (v₁ : Valuation R Γ₀) (v₂ : Valuation R Γ'₀),
  v₁.IsEquiv v₂ = ∀ (r s : R), v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s
-- Mathlib.Data.Bracket
Bracket.mk : {L : Type u_1} → {M : Type u_2} → (L → M → M) → Bracket L M
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulLeftInvariant.smulInvariantMeasure : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Mul G] [μ.IsMulLeftInvariant],
  MeasureTheory.SMulInvariantMeasure G G μ
-- Init.Data.Int.LemmasAux
Int.mul_le_mul_of_natAbs_le : ∀ {x y : ℤ} {s t : ℕ}, x.natAbs ≤ s → y.natAbs ≤ t → x * y ≤ ↑s * ↑t
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk_add_mk : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M) (x y : M) (hx : x ∈ S) (hy : y ∈ S),
  ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
-- Init.Core
Prod.map_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α) (y : γ),
  Prod.map f g (x, y) = (f x, g y)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_pow : ∀ (f : CircleDeg1Lift) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.LinearAlgebra.Pi
LinearMap.vecCons₂_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {n : ℕ} (f : M →ₗ[R] M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃) (m : M),
  (f.vecCons₂ g) m = (f m).vecCons (g m)
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_ciSup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompletePartialOrderSup α] [SupConvergenceClass α] {f : ι → α},
  Antitone f → BddAbove (Set.range f) → Filter.Tendsto f Filter.atBot (nhds (⨆ i, f i))
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Differentiable.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ},
  Differentiable ℂ f → (∀ (x : E), f x ∈ Complex.slitPlane) → Differentiable ℂ fun t => Complex.log (f t)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_eq_zero : ∀ {n : Type u_3} {α : Type v} [inst : MulZeroClass α] [NoZeroDivisors α] {a b : n → α},
  Matrix.vecMulVec a b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousLinearMap.const_apply_apply : ∀ (R : Type u_3) {M : Type u_5} [inst : TopologicalSpace M] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : ContinuousAdd M] [inst_4 : Module R M] [inst_5 : ContinuousConstSMul R M] (α : Type u_7)
  [inst_6 : TopologicalSpace α] (m : M) (x : α), ((ContinuousLinearMap.const R α) m) x = m
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id._auto_1) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv
      (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) h) =
    h
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.colimitCommGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.FilteredColimits.colimitCommGroup F = { toGroup := (CommGrpCat.FilteredColimits.G F).str, mul_comm := ⋯ }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k)[a]? = if (k == a) = true then none else m[a]?
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Units.inv_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [MulPosMono R] [PosMulMono R]
  {u : Rˣ}, ↑u⁻¹ < 0 ↔ ↑u < 0
-- Lean.Elab.Arg
Lean.Elab.Term.instToStringArg : ToString Lean.Elab.Term.Arg
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P : C}
  {f g : ⊥_ C ⟶ P}, f = g ↔ True
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_one : Complex.log 1 = 0
-- Mathlib.Data.Finset.Defs
Finset.exists_of_ssubset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊂ s₂ → ∃ x ∈ s₂, x ∉ s₁
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projl_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L),
  (LieAlgebra.SemiDirectSum.projl ψ) x = x.left
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedState.default : Lean.Parser.ParserExtension.State
-- Mathlib.Tactic.ProxyType
/-- Navigates into the sum type that we create in `mkCType` for the given constructor index.  -/
_private.Mathlib.Tactic.ProxyType.0.Mathlib.ProxyType.defaultMkProxyType.wrapSumAccess : ℕ → ℕ → Lean.Term → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Analysis.Normed.Group.Quotient
/-- `S.normedMk` satisfies `IsQuotient`.  -/
NormedAddGroupHom.isQuotientQuotient : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), S.normedMk.IsQuotient
-- Std.Do.SPred.Notation.Basic
/-- Escapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers
and connectives.
 -/
Std.Do.«termTerm(_)» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (U : Submodule R M)
  (x y : M), (x ≡ y [SMOD U]) = (Submodule.Quotient.mk x = Submodule.Quotient.mk y)
-- Mathlib.Data.Fin.Fin2
/-- `Fin2` is equivalent to the usual encoding of `Fin` as a subtype of `ℕ`.  -/
Fin2.equivFin : (n : ℕ) → Fin2 n ≃ Fin n
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.getBinderName : Lean.Expr → Lean.MetaM Lean.Name
-- Lean.Elab.Do.Basic
/-- The expression ``pure (α:=α) e``.  -/
Lean.Elab.Do.mkPureApp : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.TreeSet.ofList l cmp ↔ l.contains k = true
-- Mathlib.Computability.Language
Language.sub_def : ∀ {α : Type u_1} (l m : Language α), l - m = l \ m
-- Mathlib.Algebra.Polynomial.Reverse
_private.Mathlib.Algebra.Polynomial.Reverse.0.Polynomial.reflect.match_1.splitter : {R : Type u_1} →
  [inst : Semiring R] →
    (motive : Polynomial R → Sort u_2) →
      (x : Polynomial R) → ((f : AddMonoidAlgebra R ℕ) → motive { toFinsupp := f }) → motive x
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Technical structure theorem for monotone differentiable functions.

If a function `f` is monotone on a measurable set and has a derivative `f'`, one can decompose
the set as a disjoint union `a ∪ b ∪ c` of measurable sets where `a` is countable (the points which
are isolated on the left or on the right, where `f'` is not well controlled),
`f` is locally constant on `b` and `f' = 0` there (the preimages of the countably many points with
several preimages), and `f` is injective on `c` with nonnegative derivative (the other points).  -/
MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt : ∀ {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    MonotoneOn f s →
      (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
        ∃ a b c,
          a ∪ (b ∪ c) = s ∧
            MeasurableSet a ∧
              MeasurableSet b ∧
                MeasurableSet c ∧
                  Disjoint a (b ∪ c) ∧
                    Disjoint b c ∧
                      a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ Set.InjOn f c
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.neg_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] (s : Set α) (t : Set β),
  -s • t = -(s • t)
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.succFunEquiv_apply : ∀ (α : Type u_1) (n : ℕ) (a : Fin (n + 1) → α),
  (Fin.succFunEquiv α n) a = (fun i => a (Fin.castAdd 1 i), a (Fin.natAdd n 0))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_trans_orderIso : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] (f : α ≃*o β) (g : β ≃*o γ), ↑(f.trans g) = (↑f).trans ↑g
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.op_sub : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f g : X ⟶ Y), (f - g).op = f.op - g.op
-- Mathlib.Analysis.Distribution.Distribution
Distribution.lineDerivOp_apply_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F] (f : Distribution Ω F ⊤) (g : TestFunction Ω ℝ ⊤) (m : E),
  (LineDeriv.lineDerivOp m f) g = f (-LineDeriv.lineDerivOp m g)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a left cancel monoid if `β` is a left cancel monoid.  -/
FunLike.leftCancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : LeftCancelMonoid β] →
                [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → LeftCancelMonoid F
-- Mathlib.LinearAlgebra.Span.Defs
/-- `generator I`, if `I` is a principal submodule, is an `x ∈ M` such that `span R {x} = I`  -/
Submodule.IsPrincipal.generator : {R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (S : Submodule R M) → [S.IsPrincipal] → M
-- Init.Data.Fin.Lemmas
Fin.le_antisymm : ∀ {n : ℕ} {x y : Fin n}, x ≤ y → y ≤ x → x = y
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.mk.injEq : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (toModuleCat : ModuleCat R)
  [topologicalSpace : TopologicalSpace ↑toModuleCat] [isTopologicalAddGroup : IsTopologicalAddGroup ↑toModuleCat]
  [continuousSMul : ContinuousSMul R ↑toModuleCat] (toModuleCat_1 : ModuleCat R)
  (topologicalSpace_1 : TopologicalSpace ↑toModuleCat_1)
  (isTopologicalAddGroup_1 : IsTopologicalAddGroup ↑toModuleCat_1) (continuousSMul_1 : ContinuousSMul R ↑toModuleCat_1),
  ({ toModuleCat := toModuleCat, topologicalSpace := topologicalSpace, isTopologicalAddGroup := isTopologicalAddGroup,
        continuousSMul := continuousSMul } =
      { toModuleCat := toModuleCat_1, topologicalSpace := topologicalSpace_1,
        isTopologicalAddGroup := isTopologicalAddGroup_1, continuousSMul := continuousSMul_1 }) =
    (toModuleCat = toModuleCat_1 ∧ topologicalSpace ≍ topologicalSpace_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termX₂ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightMono_of_addRightStrictMono : ∀ (M : Type u_3) [inst : Add M] [inst_1 : PartialOrder M] [AddRightStrictMono M], AddRightMono M
-- Mathlib.GroupTheory.Congruence.Defs
/-- There is a Galois insertion of additive congruence relations on a type with
an addition `M` into binary relations on `M`.  -/
AddCon.gi : (M : Type u_1) → [inst : Add M] → GaloisInsertion addConGen DFunLike.coe