mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
/-- Interpret `ρ → m α` as an element of `ReaderT ρ m α`.
 -/
ReaderT.mk : {ρ : Type u} → {m : Type u → Type v} → {α : Type u} → (ρ → m α) → ReaderT ρ m α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' fallback : α} {f : β → β},
  (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `Metric.ediam_closure`. -/
EMetric.diam_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (s : Set α), Metric.ediam (closure s) = Metric.ediam s
-- Mathlib.Order.Category.PartOrd
PartOrd.ext_iff : ∀ {X Y : PartOrd} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Order.Hom.WithTopBot
/-- Embedding into `WithTop α`.  -/
Function.Embedding.coeWithTop : {α : Type u_1} → α ↪ WithTop α
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_sub : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ContinuousAt (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.cuspFunction h (f - g) = UpperHalfPlane.cuspFunction h f - UpperHalfPlane.cuspFunction h g
-- Mathlib.Algebra.Lie.Abelian
LieModule.IsTrivial.trivial : ∀ {L : Type v} {M : Type w} {inst : Bracket L M} {inst_1 : Zero M} [self : LieModule.IsTrivial L M] (x : L) (m : M),
  ⁅x, m⁆ = 0
-- Init.Data.BitVec.Lemmas
/-- The absolute value of `(x : BitVec w)`, when interpreted as an integer,
is the absolute value of `x.toInt` when `(x ≠ intMin)`.
 -/
BitVec.toInt_abs_eq_natAbs_of_ne_intMin : ∀ {w : ℕ} {x : BitVec w}, x ≠ BitVec.intMin w → x.abs.toInt = ↑x.toInt.natAbs
-- Mathlib.Algebra.GradedMonoid
/-- One has grade zero  -/
SetLike.GradedOne.one_mem : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {inst : SetLike S R} {inst_1 : One R} {inst_2 : Zero ι} {A : ι → S}
  [self : SetLike.GradedOne A], 1 ∈ A 0
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.toMatrixOrthonormal_reindex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {m : Type u_5} {n : Type u_6} [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) (e : n ≃ m) (f : E →ₗ[𝕜] E),
  (LinearMap.toMatrixOrthonormal (v₁.reindex e)) f = (Matrix.reindex e e) ((LinearMap.toMatrixOrthonormal v₁) f)
-- Mathlib.Computability.StateTransition
/-- A simpler version of `Respects` when the state transition relation `tr` is a function.  -/
StateTransition.FRespects : {σ₁ : Type u_1} → {σ₂ : Type u_2} → (σ₂ → Option σ₂) → (σ₁ → σ₂) → σ₂ → Option σ₁ → Prop
-- Mathlib.Computability.Partrec
Nat.rfind_zero_none : ∀ (p : ℕ →. Bool), p 0 = Part.none → Nat.rfind p = Part.none
-- Batteries.Data.String.Legacy
/-- Returns the last character in `s`. If `s = ""`, returns `(default : Char)`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.back`.

Examples:
* `"abc".back = 'c'`
* `"".back = (default : Char)`
 -/
String.Legacy.back : String → Char
-- Mathlib.Analysis.Normed.Group.Indicator
enorm_indicator_eq_indicator_enorm : ∀ {α : Type u_1} {ε : Type u_2} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f : α → ε)
  (a : α), ‖s.indicator f a‖ₑ = s.indicator (fun a => ‖f a‖ₑ) a
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.reg.sizeOf_spec : sizeOf Mathlib.Explode.Status.reg = 1
-- Mathlib.Algebra.Order.SuccPred.WithBot
WithBot.succ_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : AddMonoidWithOne α] [inst_3 : SuccAddOrder α],
  WithBot.succ 0 = 1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {q : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.Supports S q →
    Turing.PartrecToTM2.trStmts₁ q ⊆ S → Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.trStmts₁ q) S
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Try to unfold ground term in the ground/symbolic evaluator.
 -/
Lean.Meta.Simp.sevalGround : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Sets.Opens
/-- The interior of a set, as an element of `Opens`.  -/
TopologicalSpace.Opens.interior : {α : Type u_2} → [inst : TopologicalSpace α] → Set α → TopologicalSpace.Opens α
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
AlgHom.codRestrict.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f f_1 : A →ₐ[R] B) (e_f : f = f_1) (S : Subalgebra R B)
  (hf : ∀ (x : A), f x ∈ S), f.codRestrict S hf = f_1.codRestrict S ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s * t).inf f = t.inf fun y => s.inf fun x => f (x * y)
-- Init.Grind.AC
Lean.Grind.AC.Seq.contains_k_var : ∀ (y x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var y).contains_k x = (x == y)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion_finset₀ : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α},
  (↑s).Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f) →
    (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_union_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.Order.Hom.WithTopBot
OrderEmbedding.withBotMap_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), ⇑f.withBotMap = WithBot.map ⇑f
-- Init.Data.BitVec.Bitblast
BitVec.not_add_eq_not_neg : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x + y) = ~~~x - y
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- A constructor that assumes `‖z‖ < 1` instead of `dist z 0 < 1` and returns an element
of `𝔻` instead of `↥Metric.ball (0 : ℂ) 1`.  -/
Complex.UnitDisc.mk : (z : ℂ) → ‖z‖ < 1 → Complex.UnitDisc
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.ofExact_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₑ D), (CategoryTheory.RightExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }
-- Aesop.Rule.Name
Aesop.instBEqPhaseName : BEq Aesop.PhaseName
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_mul_right_right : ∀ (m n k : ℕ), m.Coprime (n + k * m) ↔ m.Coprime n
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.instAddEquivClass : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G},
  AddEquivClass (S.Equiv S') E E'
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with subtraction.  -/
Real.circleAverage_fun_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f₁ c R →
    CircleIntegrable f₂ c R →
      Real.circleAverage (fun z => f₁ z - f₂ z) c R = Real.circleAverage f₁ c R - Real.circleAverage f₂ c R
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.ker_mk' : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], (QuotientGroup.mk' N).ker = N
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds_of_ne_of_ne : ∀ {α : Type u_1} {xs : Array α} {i j k : ℕ},
  k ≠ i → k ≠ j → ∀ (hk : k < (xs.swapIfInBounds i j).size), (xs.swapIfInBounds i j)[k] = xs[k]
-- Mathlib.Algebra.MonoidAlgebra.Lift
MonoidAlgebra.liftNC_one : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Semiring k] [inst_2 : One G]
  {g_hom : Type u_6} [inst_3 : FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom),
  (MonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorphOn.preimage_interior_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 →
    ∀ {f : M → N} {s : Set M},
      IsLocalDiffeomorphOn I I' n f s → f ⁻¹' ModelWithCorners.interior N ∩ s = ModelWithCorners.interior M ∩ s
-- Mathlib.Topology.Algebra.Support
mulTSupport_subset_comp : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : One α] [inst_1 : TopologicalSpace X] [inst_2 : One β]
  {g : α → β}, (∀ {x : α}, g x = 1 → x = 1) → ∀ (f : X → α), mulTSupport f ⊆ mulTSupport (g ∘ f)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkRefl : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₂.eq_1 : ∀ (w x : UInt8),
  ByteArray.utf8DecodeChar?.verify₂ w x =
    if ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true then false
    else
      have r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x;
      decide (128 ≤ r)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z},
  CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.W.mk_dest : ∀ {P : PFunctor.{uA, uB}} (p : P.W), PFunctor.W.mk p.dest = p
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.instEDist : {α : Type u_1} → {β : Type u_2} → [PseudoEMetricSpace β] → EDist (UniformFun α β)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_δ_self'_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)},
  j = i.castSucc →
    ∀ {Z : SimplexCategory} (h : { len := n + 1 + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) h)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.range_comp_le_range : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : NonUnitalNonAssocSemiring C] [inst_8 : Module R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] C),
  NonUnitalStarAlgHom.range (g.comp f) ≤ NonUnitalStarAlgHom.range g
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsMonoidalStable.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : CategoryTheory.MonoidalCategory C] [toIsMonoidal : P.IsMonoidal]
  [toIsStableUnderAssociator : P.IsStableUnderAssociator] [toIsStableUnderUnitor : P.IsStableUnderUnitor],
  P.IsMonoidalStable
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.instCoeSet : {X : Type u_1} → [inst : MetricSpace X] → Coe (Delone.DeloneSet X) (Set X)
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.attrs : Lean.Elab.Modifiers → Array Lean.Elab.Attribute
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.iUnion_openCell_eq_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C] (n : ℕ∞),
  ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeletonLT C n)
-- Init.Data.Fin.Lemmas
Fin.cast.congr_simp : ∀ {n m : ℕ} (eq : n = m) (i i_1 : Fin n), i = i_1 → Fin.cast eq i = Fin.cast eq i_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- `spineToSimplex` is a left inverse to `spine X n`.  -/
SSet.StrictSegal.spineToSimplex_spine : ∀ {X : SSet} (self : X.StrictSegal) (n : ℕ), self.spineToSimplex ∘ X.spine n = id
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instFrame : {α : Type u} → {β : Type v} → [Order.Frame α] → [Order.Frame β] → Order.Frame (α × β)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiff.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n g → (∀ (x : E), f x ≠ 0) → ContDiff ℝ n fun x => f x ^ g x
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatters_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α},
  𝒜.Shatters s ↔ Finset.image (fun t => s ∩ t) 𝒜 = s.powerset
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, any morphism that turns to zero when precomposed with the kernel of an
epimorphism factors through that epimorphism.  -/
CategoryTheory.Abelian.epiDesc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [CategoryTheory.Epi f] →
            {T : C} →
              (g : X ⟶ T) → CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0 → (Y ⟶ T)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.compRight_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {e f : u ⟶ v} (h : CategoryTheory.Arrow.RightHomotopy e f) (g : v ⟶ w),
  (h.compRight g).hom = CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g)
-- Mathlib.Data.Int.Bitwise
Int.bodd_two : Int.bodd 2 = false
-- Lean.Util.LeanOptions
Lean.LeanOption.mk.injEq : ∀ (name : Lean.Name) (value : Lean.LeanOptionValue) (name_1 : Lean.Name) (value_1 : Lean.LeanOptionValue),
  ({ name := name, value := value } = { name := name_1, value := value_1 }) = (name = name_1 ∧ value = value_1)
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_zpow : ∀ {α : Type u} [inst : DivInvMonoid α] (z : ℤ) (a : α), Additive.ofMul (a ^ z) = z • Additive.ofMul a
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Icc_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p), Finset.Icc a b = Finset.subtype p (Finset.Icc ↑a ↑b)
-- Mathlib.Data.Multiset.Defs
Multiset.pmap_congr : ∀ {α : Type u_1} {β : Type v} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (s : Multiset α)
  {H₁ : ∀ a ∈ s, p a} {H₂ : ∀ a ∈ s, q a},
  (∀ a ∈ s, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → Multiset.pmap f s H₁ = Multiset.pmap g s H₂
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_stabilize : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n m : ℕ} {ω : Ω},
  n ≤ m → MeasureTheory.lowerCrossingTime a b f N n ω = N → MeasureTheory.lowerCrossingTime a b f N m ω = N
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
/-- `TensorProduct.comm` preserves tensor products of quadratic forms.  -/
QuadraticForm.tensorComm : {R : Type uR} →
  {M₁ : Type uM₁} →
    {M₂ : Type uM₂} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                [inst_5 : Invertible 2] →
                  (Q₁ : QuadraticForm R M₁) →
                    (Q₂ : QuadraticForm R M₂) → QuadraticMap.IsometryEquiv (Q₁.tmul Q₂) (Q₂.tmul Q₁)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_univ : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G), f.restr Set.univ = f
-- Mathlib.Data.Finset.Sups
Finset.infs_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α},
  (s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.slash_action_eqn' : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [Γ.HasDetOne]
  [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) ℝ},
  γ ∈ Γ → ∀ (z : UpperHalfPlane), f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift.unique : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ : MultilinearMap R s E} {φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E},
  (∀ (f : (i : ι) → s i), φ' ((PiTensorProduct.tprod R) f) = φ f) → φ' = PiTensorProduct.lift φ
-- Mathlib.Analysis.Complex.Harmonic.Poisson
/-- **Poisson integral formula** for harmonic functions on arbitrary disks in the complex plane,
formulated with the real part of the Herglotz–Riesz kernel of integration.
 -/
InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul : ∀ {f : ℂ → ℝ} {c w : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R) →
    w ∈ Metric.ball c R → Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w • f) c R = f w
-- Mathlib.Algebra.Order.Group.Synonym
toColex_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), toColex (a ^ b) = toColex a ^ b
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.evalAddMonoidHom_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} (a : M) (f : M →ₛₗ[σ₁₂] M₂), (LinearMap.evalAddMonoidHom a) f = f a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α}, a ∉ ∅
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.Nondegenerate.separatingRight : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] {M : Matrix m n R}, M.Nondegenerate → M.SeparatingRight
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G → M` satisfies the multiplicative 1-coboundary condition if there's `x : M`
such that `g • x / x = f(g)` for all `g : G`.  -/
groupCohomology.IsMulCoboundary₁ : {G : Type u_1} → {M : Type u_2} → [CommGroup M] → [SMul G M] → (G → M) → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
  (m.alter k f)[k']! = if (k == k') = true then (f m[k]?).get! else m[k']!
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_right_of_ge' : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atBot → (∀ᶠ (x : α) in l, g x ≤ C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Lean.Parser.Command
Lean.Parser.Command.definition : Lean.Parser.Parser
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeEndWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.takeEndWhile pat = s ↔ s.revAll pat = true
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_base : ∀ {p : ℕ}, 1 < p → padicValNat p p = 1
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_const_mul_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => b * f x) l (nhds (b * c)) ↔ Filter.Tendsto f l (nhds c)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Roc α → Std.DTreeMap.Internal.Unit.RocSliceData α
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Ioi : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α} [NoMaxOrder α], IsConnected (Set.Ioi a)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.instFullObjPostOfFaithful : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Faithful] [F.Full], (CategoryTheory.Over.post F).Full
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.instLawfulFunctor : LawfulFunctor PMF
-- Mathlib.Algebra.Group.Defs
npowRec'.eq_1 : ∀ {M : Type u_2} [inst : One M] [inst_1 : Mul M] (x : M), npowRec' 0 x = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : Lean.ToJson Lean.Lsp.CallHierarchyOutgoingCallsParams
-- Mathlib.CategoryTheory.Category.Pointed
/-- the underlying type  -/
Pointed.X : Pointed → Type u
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n g x → f x ≠ 0 → ContDiffAt ℝ n (fun x => f x ^ g x) x
-- Mathlib.Analysis.Polynomial.Norm
/-- The direct definition of the supNorm  -/
Polynomial.supNorm_def' : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A),
  p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circle average of a continuous function is itself continuous, as a function
of the radius.
 -/
Real.Continuous.circleAverage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {c : ℂ} {f : ℂ → E},
  Continuous f → Continuous (Real.circleAverage f c)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
  ⊥ < a → (a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.LucasLehmerTest.eq_1 : ∀ (p : ℕ), LucasLehmerTest p = (lucasLehmerResidue p = 0)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_neg : ∀ (R : Type u) {M : Type v} [inst : NegZeroClass R] [inst_1 : Neg M] (m : M),
  TrivSqZeroExt.inr (-m) = -TrivSqZeroExt.inr m
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring 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₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (x : M × M₂), (f.coprod g) x = f x.1 + g x.2
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α],
  Colex.instDivisionCommMonoid = { toDivisionMonoid := Colex.instDivisionMonoid, mul_comm := ⋯ }
-- Mathlib.Order.Lattice.Congruence
/-- The kernel of a lattice homomorphism as a lattice congruence.  -/
LatticeCon.ker : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Lattice α] → [inst_1 : Lattice β] → [inst_2 : FunLike F α β] → [LatticeHomClass F α β] → F → LatticeCon α
-- Mathlib.Algebra.Order.Interval.Basic
instInvInterval.eq_1 : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α],
  instInvInterval = { inv := WithBot.map Inv.inv }