mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k : α} {f : β → β} {h : k ∈ m.modify k f}, (m.modify k f).getKey k h = k
-- Init.Data.Int.DivMod.Lemmas
Int.sub_fmod_right : ∀ (a b : ℤ), (a - b).fmod b = a.fmod b
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_int_gt : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R), ∃ n, x < ↑n
-- Mathlib.GroupTheory.OrderOfElement
pow_mod_natCard : ∀ {G : Type u_6} [inst : Group G] (a : G) (n : ℕ), a ^ (n % Nat.card G) = a ^ n
-- Batteries.Data.Nat.Bisect
Nat.bisect_true : ∀ {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  p (Nat.bisect h hstart hstop) = true
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.

See also `Module.finBasis`.
 -/
Basis.ofRankEqZero : {K : Type u} →
  {V : Type v} →
    [inst : Ring K] →
      [StrongRankCondition K] →
        [inst_2 : AddCommGroup V] →
          [inst_3 : Module K V] →
            [Module.Free K V] → {ι : Type u_1} → [IsEmpty ι] → Module.rank K V = 0 → Module.Basis ι K V
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.opOp_apply : ∀ (R : Type u_7) [inst : Add R] [inst_1 : Mul R] (a : R), (RingEquiv.opOp R) a = MulOpposite.op (MulOpposite.op a)
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_submodule_of_noetherian : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), IsNoetherian R M → IsNoetherian R ↥N
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf_hom_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.RightLift f g),
  t.whiskerOfIdCompIsoSelf.hom.left = (CategoryTheory.Bicategory.leftUnitor t.lift).hom
-- Mathlib.RingTheory.Algebraic.Basic
/-- A special case of `Transcendental.restrictScalars`. This is extracted as a theorem
because in some cases `Transcendental.restrictScalars` will just runs out of memory.  -/
Transcendental.of_tower_top_of_subalgebra_le : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A ≤ B → ∀ {x : S}, Transcendental (↥B) x → Transcendental (↥A) x
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.isBaseChange_of_formallyEtale : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  [Algebra.FormallyEtale S T], IsBaseChange T (KaehlerDifferential.map R R S T)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alterₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] (k : α) (f : Option β → Option β)
  (t : Std.DTreeMap.Internal.Impl α fun x => β) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.Const.alterₘ k f t h =
    (Std.DTreeMap.Internal.Impl.updateCell k (Std.DTreeMap.Internal.Cell.Const.alter f) t h).impl
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.relIso_enum : ∀ {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s] (f : r ≃r s)
  (o : Ordinal.{u}) (hr : o < Ordinal.type r), f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.enum s) ⟨o, ⋯⟩
-- Mathlib.Data.Int.ModEq
Int.ModEq.instRefl : ∀ {n : ℤ}, Std.Refl n.ModEq
-- Mathlib.Algebra.Algebra.Prod
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.  -/
AlgHom.prodEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [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] → (A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C)
-- Mathlib.MeasureTheory.SetSemiring
/-- **Alias** of `MeasureTheory.IsSetSemiring.sdiff_mem_supClosure`. -/
MeasureTheory.IsSetSemiring.diff_mem_supClosure : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → s \ t ∈ supClosure C
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a : EInt) (X : C),
  CategoryTheory.IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))
-- Init.Data.SInt.Lemmas
Int16.toInt16_toInt32 : ∀ (n : Int16), n.toInt32.toInt16 = n
-- Mathlib.Order.Booleanisation
Booleanisation.compl_comp : ∀ {α : Type u_1} (a : α), (Booleanisation.comp a)ᶜ = Booleanisation.lift a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).maxKey?.isSome = t.maxKey?.isSome
-- Mathlib.MeasureTheory.Function.UnifTight
/-- A constant sequence is tight.  -/
MeasureTheory.unifTight_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {g : α → β},
  p ≠ ⊤ → MeasureTheory.MemLp g p μ → MeasureTheory.UnifTight (fun x => g) p μ
-- Mathlib.Data.ZMod.ValMinAbs
namedPattern.congr_simp : ∀ {α : Sort u} (x x_1 : α) (e_x : x = x_1) (a a_1 : α) (e_a : a = a_1) (h : x = a),
  namedPattern x a h = namedPattern x_1 a_1 ⋯
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.GeometricallyReduced f] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.IsReduced Y] [Finite ↑(irreducibleComponents ↥Y)], AlgebraicGeometry.IsReduced X
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_le_log : ∀ {x y : ℝ}, 0 < x → x ≤ y → Real.log x ≤ Real.log y
-- Mathlib.Data.Finsupp.Lex
Finsupp.lex_iff_of_unique : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : Unique α] [inst_2 : LT N] {r : α → α → Prop} [Std.Irrefl r]
  {x y : α →₀ N}, Finsupp.Lex r (fun x1 x2 => x1 < x2) x y ↔ x default < y default
-- Mathlib.Algebra.Group.Defs
AddCommSemigroup.toAddCommMagma : {G : Type u} → [self : AddCommSemigroup G] → AddCommMagma G
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n),
  T.Iff (φ ⊔ ψ) (φ.not ⊓ ψ.not).not
-- Mathlib.RingTheory.RingHom.OpenImmersion
/-- A standard open immersion is one that is a localization map away from some element.  -/
Algebra.IsStandardOpenImmersion : (R : Type u_4) → (S : Type u_5) → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → [Algebra R S] → Prop
-- Lean.Server.Completion.CompletionCollectors
/-- Converts `n` to `Name.anonymous` if `n` is a private prefix (see `Lean.isPrivatePrefix`).
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.stripPrivatePrefix : Lean.Name → Lean.Name
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator : (α : Type) →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (β : Std.Sat.AIG α → ℕ → Type) →
        ({len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len) → Prop
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.nhds_eq_map_inclusion : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S)
      (x : RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S)),
      nhds (RestrictedProduct.inclusion R A hS x) = Filter.map (RestrictedProduct.inclusion R A hS) (nhds x)
-- Init.Data.Vector.Lemmas
Vector.foldl_map : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {n : ℕ} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Vector β₁ n} {init : α},
  Vector.foldl g init (Vector.map f xs) = Vector.foldl (fun x y => g x (f y)) init xs
-- Batteries.Classes.Order
/-- `le` is total: either `le a b` or `le b a`.  -/
Batteries.TotalBLE.total : ∀ {α : Sort u_1} {le : α → α → Bool} [self : Batteries.TotalBLE le] {a b : α}, le a b = true ∨ le b a = true
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.getChildNgen.match_1.eq_1 : ∀ (motive : Lean.NameGenerator × Lean.NameGenerator → Sort u_1) (cngen ngen : Lean.NameGenerator)
  (h_1 : (cngen ngen : Lean.NameGenerator) → motive (cngen, ngen)),
  (match (cngen, ngen) with
    | (cngen, ngen) => h_1 cngen ngen) =
    h_1 cngen ngen
-- Mathlib.Algebra.Order.ZeroLEOne
Pi.instZeroLEOneClass : ∀ {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → Zero (R i)] [inst_1 : (i : ι) → One (R i)]
  [inst_2 : (i : ι) → LE (R i)] [∀ (i : ι), ZeroLEOneClass (R i)], ZeroLEOneClass ((i : ι) → R i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.any_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {p : (a : α) → β a → Bool},
  ((↑m).toList.any fun x => p x.fst x.snd) = (↑m).any p
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient by a discontinuous group action of a locally compact T₂
space is T₂.  -/
t2Space_of_properlyDiscontinuousVAdd_of_t2Space : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T] [T2Space T]
  [LocallyCompactSpace T] [ContinuousConstVAdd Γ T] [ProperlyDiscontinuousVAdd Γ T],
  T2Space (Quotient (AddAction.orbitRel Γ T))
-- Qq.Macro
Qq.Impl.unquoteLevel : Lean.Expr → Qq.Impl.UnquoteM Lean.Level
-- Init.Data.Repr
instReprNat : Repr ℕ
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C) (x : CategoryTheory.IsCofiltered.CofilteredClosureSmall.AbstractCofilteredClosure✝ f),
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization✝ f x =
    (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f x.fst).snd x.snd
-- Mathlib.Algebra.Lie.Basic
LieEquiv.refl_symm : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁],
  LieEquiv.refl.symm = LieEquiv.refl
-- Init.Data.Vector.Lemmas
Vector.toArray_insertIdx! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α},
  i ≤ n → (xs.insertIdx! i x).toArray = xs.toArray.insertIdx! i x
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_sdiff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : Subtype MeasurableSet), ↑(s \ t) = ↑s \ ↑t
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- Addition in `WithBot (WithTop α)` is right cancellative provided the element
being cancelled is not `⊤` or `⊥`.
 -/
WithBot.add_le_add_iff_right' : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α] {a b c : WithBot (WithTop α)},
  c ≠ ⊥ → c ≠ ⊤ → (a + c ≤ b + c ↔ a ≤ b)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonStaticRegistrationOptions.toJson : Lean.Lsp.StaticRegistrationOptions → Lean.Json
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.DTreeMap.Raw.minKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Option α
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The uniformity on `α →ᵤ[𝔖] β` is the same as the uniformity on `α →ᵤ β`,
provided that `Set.univ ∈ 𝔖`.

Here we formulate it as a `UniformEquiv`.  -/
UniformOnFun.uniformEquivUniformFun : {α : Type u_1} →
  (β : Type u_2) → [inst : UniformSpace β] → (𝔖 : Set (Set α)) → Set.univ ∈ 𝔖 → UniformOnFun α β 𝔖 ≃ᵤ UniformFun α β
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is filtered or empty, and we have a functor `R : C ⥤ D` with a left adjoint, then `D` is
filtered or empty.
 -/
CategoryTheory.IsFilteredOrEmpty.of_right_adjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D}
  (h : L ⊣ R), CategoryTheory.IsFilteredOrEmpty D
-- Mathlib.Algebra.Star.SelfAdjoint
/-- Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a
self-adjoint element.  -/
isSelfAdjoint_smul_of_mem_skewAdjoint : ∀ {R : Type u_1} {A : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup A] [inst_2 : Module R A]
  [inst_3 : StarAddMonoid R] [inst_4 : StarAddMonoid A] [StarModule R A] {r : R},
  r ∈ skewAdjoint R → ∀ {a : A}, a ∈ skewAdjoint A → IsSelfAdjoint (r • a)
-- Init.Data.String.Pattern.Basic
Nat.lt_wfRel.eq_1 : Nat.lt_wfRel = { rel := fun x1 x2 => x1 < x2, wf := Nat.lt_wfRel._proof_3 }
-- Mathlib.Condensed.Discrete.Characterization
/-- `LightCondSet.LocallyConstant.functor` is left adjoint to the forgetful functor from light condensed
sets to sets.
 -/
LightCondSet.LocallyConstant.adjunction : LightCondSet.LocallyConstant.functor ⊣ LightCondensed.underlying (Type u)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0.inj : ∀ {a zero a_1 zero_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 a zero =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 a_1 zero_1 →
    a = a_1 ∧ zero = zero_1
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.splitter : {β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (Option β')} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property none) → motive ⟨none, h'⟩) →
              ((out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩) → motive __do_lift
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instUnionOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Union (Std.ExtTreeSet α cmp)
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableWithinAt.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G} {x : G}, DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun y => ‖f y‖ ^ 2) s x
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.has_sdiff : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {s₁ s₂ : Set α}, d.Has s₁ → d.Has s₂ → s₂ ⊆ s₁ → d.Has (s₁ \ s₂)
-- Init.Data.UInt.Lemmas
UInt64.le_trans : ∀ {a b c : UInt64}, a ≤ b → b ≤ c → a ≤ c
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → k ∉ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_union_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α) (p : α → Prop),
  (∀ᵐ (x : α) ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂μ.restrict s, p x) ∧ ∀ᵐ (x : α) ∂μ.restrict t, p x
-- Mathlib.Probability.Process.Kolmogorov
/-- A process with the property `IsKolmogorovProcess` such that `∀ t, X t =ᵐ[P] h.mk X t`.  -/
ProbabilityTheory.IsAEKolmogorovProcess.mk : {T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      [inst : PseudoEMetricSpace T] →
        {mΩ : MeasurableSpace Ω} →
          [inst_1 : PseudoEMetricSpace E] →
            {p q : ℝ} →
              {M : NNReal} →
                {P : MeasureTheory.Measure Ω} →
                  (X : T → Ω → E) → ProbabilityTheory.IsAEKolmogorovProcess X P p q M → T → Ω → E
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The expression for the normalized 2-morphism `α ≫ η ≫ ηs`.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalExpr.consM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.WhiskerLeft →
        Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.language_eq_zero_of_forall_input_ne_initial : ∀ {T : Type u_1} {g : ContextFreeGrammar T}, (∀ r ∈ g.rules, r.input ≠ g.initial) → g.language = 0
-- Init.Data.Vector.Extract
Vector.extract_of_size_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (h : n < j), xs.extract i j = Vector.cast ⋯ (xs.extract i)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (r : R), v.intAdicAbvDef hb r = (WithZeroMulInt.toNNReal ⋯) (v.intValuation r)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.equal : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (X : CategoryTheory.Functor C V),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.pure_bind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β : Type w} {f : α → Std.Iterators.PostconditionT m β}
  {a : α}, (pure a).bind f = f a
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.f_mem_lieAlgebra : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.f i ∈ RootPairing.GeckConstruction.lieAlgebra b
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.pure.inj : ∀ {h h_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MCasesPat.pure h = Lean.Parser.Tactic.MCasesPat.pure h_1 → h = h_1
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_eq_empty : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a}, f.neLocus g = ∅ ↔ f = g
-- Mathlib.RingTheory.PicardGroup
_private.Mathlib.RingTheory.PicardGroup.0.Submodule.projective_units_and_mul'_comp_lTensor_bijective : ∀ {R : Type u} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (I : (Submodule R A)ˣ),
  Module.Projective R ↥↑I ∧ Function.Bijective ⇑(LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑I).subtype)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.forall : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {P : M ⧸ p → Prop}, (∀ (a : M ⧸ p), P a) ↔ ∀ (a : M), P (Submodule.Quotient.mk a)
-- Mathlib.Order.Preorder.Chain
Flag.chain_le : ∀ {α : Type u_1} [inst : LE α] (s : Flag α), IsChain (fun x1 x2 => x1 ≤ x2) ↑s
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Given a closed subgroup `H` of a topological group `G`, the right action of `H` on `G`
is proper. Note that the corresponding statement for the left action can be proven by
`inferInstance`.  -/
instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G}
  [H_closed : IsClosed ↑H], ProperSMul (↥H.op) G
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l : Std.DTreeMap.Internal.Impl α β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                              (h :
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
                                    false) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                  h) →
              motive x x_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.sub : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : (i : α) → E i},
  Memℓp f p → Memℓp g p → Memℓp (f - g) p
-- Mathlib.Topology.Algebra.Monoid
/-- Eta-expanded form of `Continuous.pow` -/
Continuous.fun_pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M}, Continuous f → ∀ (n : ℕ), Continuous fun i => f i ^ n
-- Mathlib.Data.Finsupp.Single
Finsupp.support_update_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) {b : M} [inst_1 : DecidableEq α],
  (f.update a b).support ⊆ insert a f.support
-- Init.Data.ToString.Basic
instToStringRaw_1 : ToString String.Pos.Raw
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.mk.inj : ∀ {rule : Aesop.SafeRule} {output : Aesop.RuleTacOutput} {rule_1 : Aesop.SafeRule} {output_1 : Aesop.RuleTacOutput},
  { rule := rule, output := output } = { rule := rule_1, output := output_1 } → rule = rule_1 ∧ output = output_1
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hom_id : ∀ {X : AddCommGrpCat}, AddCommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = AddMonoidHom.id ↑X