mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.le_max? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {a : α} {t : RBTree.RBNode α} [Std.TransCmp cmp],
  RBTree.RBNode.Ordered cmp t → t.max? = some a → ∀ x ∈ t, cmp x a ≠ Ordering.gt
-- Mathlib.Tactic.GCongr.Core
/-- Attribute marking "generalized congruence" (`gcongr`) lemmas.  Such lemmas must have a
conclusion of a form such as `f x₁ y z₁ ∼ f x₂ y z₂`; that is, a relation between the application of
a function to two argument lists, in which the "varying argument" pairs (here `x₁`/`x₂` and
`z₁`/`z₂`) are all free variables. These lemmas are used by the `gcongr` and `grw` tactics.

The antecedents of such a lemma are classified as generating "main goals" if they are of the form
`x₁ ≈ x₂` for some "varying argument" pair `x₁`/`x₂` (and a possibly different relation `≈` to `∼`),
or more generally of the form `∀ i h h' j h'', f₁ i j ≈ f₂ i j` (say) for some "varying argument"
pair `f₁`/`f₂`, where the arguments of `f₁` and `f₂` are the same list of variables which have to
be bound by the preceding `∀`. (Other antecedents are considered to generate "side goals".)

If a lemma such as `add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d` has been tagged with `gcongr`,
then a direct consequence like `a ≤ b → a + c ≤ b + c` does *not* need to be tagged.
However, if a more specific lemma has fewer side conditions, it should also be tagged with `gcongr`.
For example, `mul_le_mul_of_nonneg_right` and `mul_le_mul_of_nonneg_left` are both tagged.

* `gcongr only` relaxes some checks that ensure that the lemma is suitable for use in `grw`.
  So, a lemma tagged `gcongr only` is not used by `grw`, but it may still be used by `gcongr`.
* `gcongr strict` lets you tag lemmas where the conclusion relates two different constants,
  instead of a constant with itself.
  This allows `grw` to replace one constant with another while doing a rewrite.
  In particular, we use this to have special support for rewriting with strict inequalities (`<`).
  This is done by applying `gcongr strict` to `lt_of_lt_of_le`, which has the conclusion
  `b ≤ c → a < c` that relates `LE.le` with `LT.lt` (and similarly for `lt_of_lt_of_le'`).
  As a result, a rewrite with a strict inequality can turn `<` into `≤`, or `≤` into `<`,
  depending on whether this appears in positive or negative position.
 -/
Mathlib.Tactic.GCongr.gcongrAttr : Lean.ParserDescr
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.le.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((val : β) → motive none (some val)) →
            (Unit → motive none none) →
              ((val : α) → motive (some val) none) → ((x : α) → (y : β) → motive (some x) (some y)) → motive x x_1
-- Mathlib.Topology.Subpath
/-- Concatenating `n + 1` paths corresponds to concatenating `n` paths and then the last path.  -/
Path.concat_succ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} (p : Fin (n + 2) → X)
  (F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)),
  Path.concat p F = (Path.concat (p ∘ Fin.castSucc) fun k => F k.castSucc).trans (F (Fin.last n))
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_lt_top : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep < ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ⊤
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x y y' : MonCat.Colimits.Prequotient F) (x_1 : MonCat.Colimits.Relation F y y'),
  MonCat.Colimits.Relation.below x_1 → motive y y' x_1 → MonCat.Colimits.Relation.below ⋯
-- Std.Net.Addr
Std.Net.instInhabitedIPv6Addr : Inhabited Std.Net.IPv6Addr
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.fixedPt_neg : ∀ {g : GL (Fin 2) ℝ} (hg : (-g).IsElliptic), UpperHalfPlane.fixedPt (-g) hg = UpperHalfPlane.fixedPt g ⋯
-- Mathlib.Algebra.CharP.Invertible
CharP.isUnit_intCast_iff : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] {z : ℤ}, Nat.Prime p → (IsUnit ↑z ↔ ¬↑p ∣ z)
-- Std.Data.ExtTreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtTreeSet.get! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.GroupTheory.Exponent
/-- The exponent of a submonoid `H ≤ G` divides the exponent of `G`.
 -/
Monoid.exponent_submonoid_dvd : ∀ {G : Type u} [inst : Monoid G] (H : Submonoid G), Monoid.exponent ↥H ∣ Monoid.exponent G
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {fallback : β} {f : Option β → Option β},
  (t.alter k f).getD k' fallback = if cmp k k' = Ordering.eq then (f t[k]?).getD fallback else t.getD k' fallback
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If self-maps `f` and `g` commute, then `g` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `Function.bijOn_fixedPoints_comp`.  -/
Function.Commute.right_bijOn_fixedPoints_comp : ∀ {α : Type u_1} {f g : α → α},
  Function.Commute f g → Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddMonoidHom.tendsto_coe_cofinite_of_discrete : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : Type u_2}
  [inst_4 : AddGroup H] {f : H →+ G},
  Function.Injective ⇑f → IsDiscrete ↑f.range → Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` have power series `q` and `p` respectively at `f x` and `x`,
then `g ∘ f` admits the power series `q.comp p` at `x`.  -/
HasFPowerSeriesAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt g q (f x) → HasFPowerSeriesAt f p x → HasFPowerSeriesAt (g ∘ f) (q.comp p) x
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_iUnion : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {ι : Sort u_3} (s : ι → Set M),
  (FirstOrder.Language.Substructure.closure L).toFun (⋃ i, s i) =
    ⨆ i, (FirstOrder.Language.Substructure.closure L).toFun (s i)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : m) (j : n), A.row i j = A i j
-- Mathlib.RingTheory.FiniteType
AlgHom.FiniteType.of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Function.Surjective ⇑f → f.FiniteType
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.GrindTacticM : Type → Type
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.isClosed_polar : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (s : Set E), IsClosed (StrongDual.polar 𝕜 s)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mk.injEq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (X : ι → V) (d : (i j : ι) → X i ⟶ X j)
  (shape : autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam)
  (d_comp_d' :
    autoParam (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0)
      HomologicalComplex.d_comp_d'._autoParam)
  (X_1 : ι → V) (d_1 : (i j : ι) → X_1 i ⟶ X_1 j)
  (shape_1 : autoParam (∀ (i j : ι), ¬c.Rel i j → d_1 i j = 0) HomologicalComplex.shape._autoParam)
  (d_comp_d'_1 :
    autoParam (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d_1 i j) (d_1 j k) = 0)
      HomologicalComplex.d_comp_d'._autoParam),
  ({ X := X, d := d, shape := shape, d_comp_d' := d_comp_d' } =
      { X := X_1, d := d_1, shape := shape_1, d_comp_d' := d_comp_d'_1 }) =
    (X = X_1 ∧ d ≍ d_1)
-- Mathlib.Analysis.Normed.Group.Basic
norm_eq_of_mem_sphere' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {r : ℝ} (x : ↑(Metric.sphere 1 r)), ‖↑x‖ = r
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPathConnected_closedEBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  IsPathConnected (Metric.closedEBall x r)
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.compProj_val : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {α : ODE.FunSpace t₀ x₀ r L} {t : ↑(Set.Icc tmin tmax)}, α.compProj ↑t = α.toFun t
-- Mathlib.Data.Finset.Image
Finset.attach_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α),
  (insert a s).attach = insert ⟨a, ⋯⟩ (Finset.image (fun x => ⟨↑x, ⋯⟩) s.attach)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg.sizeOf_spec : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg e p) = 1 + sizeOf e + sizeOf p
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Units.mk0_prod : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : CommGroupWithZero G₀] (s : Finset ι) (f : ι → G₀) (h : ∏ i ∈ s, f i ≠ 0),
  Units.mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, Units.mk0 (f ↑i) ⋯
-- Mathlib.Data.List.Forall2
Relator.LeftUnique.forall₂ : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, Relator.LeftUnique R → Relator.LeftUnique (List.Forall₂ R)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.toMonoidWithZeroHom_apply : ∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommMonoidWithZero R] [inst_2 : Nontrivial R]
  (χ : MulChar R R') (a : R), ↑χ a = (↑χ.toMonoidHom).toFun a
-- Mathlib.Algebra.Algebra.Operations
/-- `(span R {·})` as a `MonoidWithZeroHom`.  -/
Submodule.spanSingleton : (R : Type u) →
  [inst : CommSemiring R] → {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →*₀ Submodule R A
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.stdGaussian.congr_simp : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E], ProbabilityTheory.stdGaussian E = ProbabilityTheory.stdGaussian E
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.mul_liftRight_inv : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x))
  (x : M), f x * ↑((IsUnit.liftRight f h) x)⁻¹ = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.pi_top : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η), (AddSubgroup.pi I fun i => ⊤) = ⊤
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.instFunLike : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → FunLike (CocompactMap α β) α β
-- Mathlib.Topology.UnitInterval
unitInterval.le_symm_comm : ∀ {i j : ↑unitInterval}, i ≤ unitInterval.symm j ↔ j ≤ unitInterval.symm i
-- Lean.Declaration
Lean.InductiveVal.numCtors : Lean.InductiveVal → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
/-- The function `tanh` is meromorphic in normal form on `Set.univ`.  -/
Complex.meromorphicNFOn_tanh : MeromorphicNFOn Complex.tanh Set.univ
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyoneda_obj_map : ∀ (M : CommMonCatᵒᵖ) {X Y : CommMonCat} (f : X ⟶ Y),
  (CommMonCat.coyoneda.obj M).map f = CommMonCat.ofHom (MonoidHom.compHom (CommMonCat.Hom.hom f))
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLTOffset : LT Std.Time.Hour.Offset
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type E₆. See [bourbaki1968] plate V, page 277.  -/
CartanMatrix.E₆ : Matrix (Fin 6) (Fin 6) ℤ
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ],
  ∃ C,
    ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.isBigO_atTop_of_degree_le`. -/
Polynomial.isBigO_of_degree_le : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜], P.degree ≤ Q.degree → (fun x => Polynomial.eval x P) =O[Filter.atTop] fun x => Polynomial.eval x Q
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f),
  (CategoryTheory.MorphismProperty.Under.mk Q f hf).hom = f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateRight.inj : ∀ {n n_1 : ℕ}, Std.Tactic.BVDecide.BVUnOp.rotateRight n = Std.Tactic.BVDecide.BVUnOp.rotateRight n_1 → n = n_1
-- Mathlib.NumberTheory.Divisors
Nat.sum_properDivisors_prime_nsmul : ∀ {α : Type u_1} [inst : AddCommMonoid α] {k p : ℕ} {f : ℕ → α},
  Nat.Prime p → ∑ x ∈ (p ^ k).properDivisors, f x = ∑ x ∈ Finset.range k, f (p ^ x)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_self_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), f.natDegree ≠ 0 → f.resultant f = 0
-- Init.Data.Array.OfFn
Array.map_ofFn : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} {f : Fin n → α} {g : α → β}, Array.map g (Array.ofFn f) = Array.ofFn (g ∘ f)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffix?_eq_skipSuffix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.skipSuffix? pat = Option.map String.Pos.ofToSlice (s.toSlice.skipSuffix? pat)
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- If `∑' i, ‖f i‖` is summable, then `‖∑' i, f i‖ ≤ (∑' i, ‖f i‖)`. Note that we do not assume
that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space.  -/
norm_tsum_le_tsum_norm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
  (Summable fun i => ‖f i‖) → ‖∑' (i : ι), f i‖ ≤ ∑' (i : ι), ‖f i‖
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keysArray_insertIfNew_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {k : α}, (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k)
-- Mathlib.Analysis.RCLike.Lemmas
Polynomial.aeval_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (p : Polynomial ℝ) (x : ℝ), (Polynomial.aeval ↑x) p = ↑(Polynomial.eval x p)
-- Lean.Elab.BuiltinTerm
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.elabOptLevel : Lean.Syntax → Lean.Elab.TermElabM Lean.Level
-- Lean.Elab.DocString
/-- Environment extension for code suggestions  -/
Lean.Doc.codeSuggestionExt : Lean.SimpleScopedEnvExtension Lean.Name Lean.NameSet
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.SpecToEquivOfField_apply_snd : ∀ (K : Type u) [inst : Field K] (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X),
  ((AlgebraicGeometry.Scheme.SpecToEquivOfField K X) f).snd =
    AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo f)
-- Mathlib.Data.Set.Lattice
Set.Iic_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), Set.Iic (sInf s) = ⋂ a ∈ s, Set.Iic a
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `b` is odd, then `J(4 | b) = 1`.  -/
jacobiSym.at_four : ∀ {b : ℕ}, Odd b → jacobiSym 4 b = 1
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- If `P` is a submodule of `M` and `Q` a submodule of `N`,
and `f : M ≃ₛₗ[σ] N` maps `P` to `Q`, then `M ⧸ P` is equivalent to `N ⧸ Q`.  -/
Submodule.Quotient.equiv : {R : Type u_1} →
  [inst : Ring R] →
    {R₂ : Type u_5} →
      [inst_1 : Ring R₂] →
        {σ₁₂ : R →+* R₂} →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M : Type u_6} →
                  {N : Type u_7} →
                    [inst_4 : AddCommGroup M] →
                      [inst_5 : Module R M] →
                        [inst_6 : AddCommGroup N] →
                          [inst_7 : Module R₂ N] →
                            (P : Submodule R M) →
                              (Q : Submodule R₂ N) →
                                (f : M ≃ₛₗ[σ₁₂] N) → Submodule.map (↑f) P = Q → (M ⧸ P) ≃ₛₗ[σ₁₂] N ⧸ Q
-- Init.Data.Float.Model.Float
/-- Returns `true` if the float represents a real number, i.e., it is neither infinite nor `NaN`.
 -/
Float.Model.isFinite : Float.Model → Bool
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.revFindAux.eq_def : ∀ (s : String) (p : Char → Bool) (pos : String.Pos.Raw),
  String.Legacy.revFindAux s p pos =
    if h : pos = 0 then none
    else
      have this := ⋯;
      have pos := String.Pos.Raw.prev s pos;
      if p (String.Pos.Raw.get s pos) = true then some pos else String.Legacy.revFindAux s p pos
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => ↑(|X ω| ^ p) * Complex.exp (z * ↑(X ω))) μ
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.withBotCoe : {ι : Type u_1} → CoeTC (WithBot (BoxIntegral.Box ι)) (Set (ι → ℝ))
-- Mathlib.Data.Set.Prod
Set.offDiag_union : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measure `μ` on a quotient satisfies `AddQuotientMeasureEqMeasurePreimage`
with respect to a sigma-finite measure `ν`, then it is itself `SigmaFinite`.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  [i : MeasureTheory.SigmaFinite ν] [i' : MeasureTheory.HasAddFundamentalDomain G α ν]
  (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ], MeasureTheory.SigmaFinite μ
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- **Alias** of `aeconst_of_dense_setOfPred_preimage_smul_ae`.

---

Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull.  -/
aeconst_of_dense_setOf_preimage_smul_ae : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g • x) ⁻¹' s =ᵐ[μ] s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
tendsto_measure_Icc : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.NullSingletonClass μ]
  (b : ℝ), Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (nhds 0) (nhds 0)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.natDegree_map_le : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  (Polynomial.map f p).natDegree ≤ p.natDegree
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.instMulAction_1 : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      (φ : ↥A ≃* ↥B) →
        {d : HNNExtension.NormalWord.TransversalPair G A B} →
          MulAction (HNNExtension G A B φ) (HNNExtension.NormalWord d)
-- Lean.Message
Lean.ToMessageData.toMessageData : {α : Type} → [self : Lean.ToMessageData α] → α → Lean.MessageData
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- A path induces an injective homomorphism from a path graph to the graph  -/
SimpleGraph.Walk.IsPath.pathGraphCopy : {V : Type u_3} →
  [DecidableEq V] →
    {G : SimpleGraph V} → {u v : V} → {w : G.Walk u v} → w.IsPath → (SimpleGraph.pathGraph (w.length + 1)).Copy G
-- Mathlib.Topology.ExtremallyDisconnected
CompactT2.projective_iff_extremallyDisconnected : ∀ {A : Type u} [inst : TopologicalSpace A] [CompactSpace A] [T2Space A],
  CompactT2.Projective A ↔ ExtremallyDisconnected A
-- Lean.Widget.InteractiveGoal
Lean.Widget.instInhabitedInteractiveHypothesisBundle.default : Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.NumberTheory.NumberField.CMField
IsCyclotomicExtension.Rat.instIsCMFieldOfTopSetNatRat : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [IsCyclotomicExtension ⊤ ℚ K], NumberField.IsCMField K
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- If `f` is periodic wrt a ℤ-lattice, then the range of `f` is compact.  -/
IsZLattice.isCompact_range_of_periodic : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : TopologicalSpace F] (L : Submodule ℤ E) [inst_4 : DiscreteTopology ↥L] [IsZLattice ℝ L] (f : E → F),
  Continuous f → (∀ (z w : E), w ∈ L → f (z + w) = f z) → IsCompact (Set.range f)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.natDegree 1 = 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvolutiveInv.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : InvolutiveInv G],
  Filter.Germ.instInvolutiveInv = { toInv := Filter.Germ.instInv, inv_inv := ⋯ }
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.μ_nonempty : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {s : ℕ → ℕ},
  (∀ (n : ℕ), s n ≤ n) →
    ∀ {x : R} (ψ : ℕ → ℕ),
      {a | ∀ᶠ (n : ℝ) in Filter.map (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) Filter.atTop, n ≤ a}.Nonempty
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.pi_ge' : ∀ {x : ℝ}, 1 < x → ((x - 1) * Real.log 2 - Real.log (x + 2)) / Real.log x ≤ ↑⌊x⌋₊.primeCounting
-- Init.Data.Sum.Basic
/-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`.  -/
Sum.Lex.inl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α},
  r a₁ a₂ → Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂)
-- Init.Data.UInt.Lemmas
USize.mul_succ : ∀ {a b : USize}, a * (b + 1) = a * b + a
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.finsetSum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Finset ι) (f : ι → R),
  (∀ x ∈ s, f x ∈ I) → s.sum f ∈ I
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  Differentiable 𝕜 Prod.snd
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- MetavarContext after the tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mctxAfter : Mathlib.Linter.Flexible.TacticData✝ → Lean.MetavarContext