mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- the composition of the two directions of a homotopy equivalence is
homotopic to the identity of the source  -/
CategoryTheory.ShortComplex.HomotopyEquiv.homotopyHomInvId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (self : S₁.HomotopyEquiv S₂) →
          CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp self.hom self.inv)
            (CategoryTheory.CategoryStruct.id S₁)
-- Lean.Meta.MkIffOfInductiveProp
/-- The number of equalities, or `none` in the case when we've reduced something
of the form `p ∧ True` to just `p`.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.neqs : Lean.Meta.Shape✝ → Option ℕ
-- Mathlib.Data.SetLike.Basic
/-- If `s` is a proper element of a `SetLike` structure (i.e., `s ≠ ⊤`) and the top element
coerces to the universal set, then there exists an element not in `s`.  -/
SetLike.exists_not_mem_of_ne_top : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] [inst : LE A] [inst_1 : OrderTop A] (s : A),
  s ≠ ⊤ → autoParam (↑⊤ = Set.univ) SetLike.exists_not_mem_of_ne_top._auto_1 → ∃ b, b ∉ s
-- Mathlib.LinearAlgebra.Dimension.Basic
AddEquivClass.toAddEquiv.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : AddEquivClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoPushout_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h.isoPushout.inv = inl
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.IsRightDerivedFunctor.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : F ⟶ L.comp RF),
  α = α_1 →
    ∀ (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W],
      RF.IsRightDerivedFunctor α W = RF.IsRightDerivedFunctor α_1 W_1
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.toMetricSpace : {E : Type u_8} → [self : NormedAddGroup E] → MetricSpace E
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.setLIntegral_rnDeriv_mul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → ENNReal},
      AEMeasurable f ν →
        ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_intermediateZip.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n' : ℕ) (h_1 : Unit → motive 0) (h_2 : (n' : ℕ) → motive n'.succ),
  (match n'.succ with
    | 0 => h_1 ()
    | n'.succ => h_2 n') =
    h_2 n'
-- Init.Data.Ord.Basic
Ordering.isNe_eq : Ordering.eq.isNe = false
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.SolverMode.counterexample.sizeOf_spec : sizeOf Lean.Elab.Tactic.BVDecide.SolverMode.counterexample = 1
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierInvSMul` is a function space on which the inverse Fourier transform is homogeneous.  -/
FourierInvSMul : (R : Type u_5) → (E : Type u_6) → (F : outParam (Type u_7)) → [SMul R E] → [SMul R F] → [FourierTransformInv E F] → Prop
-- Init.Data.Array.Lemmas
Array.replicate_beq_replicate : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {n : ℕ}, (Array.replicate n a == Array.replicate n b) = (n == 0 || a == b)
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_inr : ∀ {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₃), f.coprod g ∘ₗ LinearMap.inr R M M₂ = g
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.mem_support_of_ne_mem_support_of_adj_of_isPath : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic →
    ∀ {u v w : V} {p : G.Walk u v} {q : G.Walk u w}, p.IsPath → q.IsPath → G.Adj v w → v ∉ q.support → w ∈ p.support
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta₁_ne_zero_of_near_one : ∀ᶠ (s : ℂ) in nhds 1, riemannZeta₁ s ≠ 0
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.structuralIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ≅ g), η.symm.hom = η.inv
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_apply_inl : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m)
  (j : n₁), A₁.fromCols A₂ i (Sum.inl j) = A₁ i j
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.ext_iff : ∀ {M N : SemiNormedGrp₁} {x y : M.Hom N}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.op_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.op.h₃ = h.h₀.op
-- Mathlib.Data.NNRat.Floor
Mathlib.Meta.NormNum.IsRat.natCeil : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] (r : R)
  (n d : ℕ), Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsNat ⌈r⌉₊ 0
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.isCompl_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {U : Submodule R M}
  {V : Submodule R N}, p.IsPerfectCompl U V → IsCompl U (Submodule.map (↑p.toPerfPair.symm) V.dualAnnihilator)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- The fold function used for performRupCheck.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint : {n : ℕ} →
  Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
        Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool →
      ℕ →
        Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
          Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.summable_pow_mul_exp_neg_nat_mul : ∀ (k : ℕ) {r : ℝ}, 0 < r → Summable fun n => ↑n ^ k * Real.exp (-r * ↑n)
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.mk.injEq : ∀ (numClauses maxLit numClauses_1 maxLit_1 : ℕ),
  ({ numClauses := numClauses, maxLit := maxLit } = { numClauses := numClauses_1, maxLit := maxLit_1 }) =
    (numClauses = numClauses_1 ∧ maxLit = maxLit_1)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstArgInfo.mk.injEq : ∀ (isProof isInstance isProof_1 isInstance_1 : Bool),
  ({ isProof := isProof, isInstance := isInstance } = { isProof := isProof_1, isInstance := isInstance_1 }) =
    (isProof = isProof_1 ∧ isInstance = isInstance_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.DTreeMap.Const.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_5.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : Std.IterM Id s.Subslice → Sort u_1)
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.SplitIterator.atEnd }),
  (match { internalState := String.Slice.SplitIterator.atEnd } with
    | { internalState := String.Slice.SplitIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.SplitIterator.atEnd } => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Fin.Basic
/-- If you actually have an element of `Fin n`, then the `n` is always positive  -/
Fin.size_positive : ∀ {n : ℕ} (a : Fin n), 0 < n
-- Mathlib.Data.Countable.Basic
instUncountableProdOfNonempty : ∀ {α : Type u} {β : Type v} [Uncountable α] [Nonempty β], Uncountable (α × β)
-- Mathlib.Algebra.Order.Module.Defs
IsOrderedModule.toPosSMulMono : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  {inst_4 : Zero β} [self : IsOrderedModule α β], PosSMulMono α β
-- Lean.Meta.WHNF
/-- Zeta reduces `let`s/`have`s.
If `zetaHave` is false, then `have`s are not zeta reduced.

Auxiliary function for `whnfCore` and `Simp.reduceStep`, to implement the `zeta` option.
This function does not implement `zetaUnused` logic,
which is instead the responsibility of `consumeUnusedLet`.
The `expandLet` function works with expressions with loose bound variables,
and thus determining whether a let variable is used isn't an O(1) operation.

Note: since `expandLet` and `consumeUnusedLet` are separated like this, a consequence is that
in the `+zeta -zetaHave +zetaUnused` configuration, then `whnfCore` has quadratic complexity
when reducing a sequence of alternating `let`s and `have`s where the `let`s are used but the `have`s are unused.
 -/
Lean.Meta.expandLet : Lean.Expr → Array Lean.Expr → optParam Bool true → Lean.Expr
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.coverToFun : {S : Type u_4} →
  {T : Type u_5} →
    {X : Type u_6} →
      {Y : Type u_7} →
        (i : Y → T) → (π : T → S × Option X) → T ⊕ { xy // π (i xy.1) = π (i xy.2) } → { xy // π xy.1 = π xy.2 }
-- Mathlib.Data.Int.GCD
Nat.gcdB_zero_left : ∀ {s : ℕ}, Nat.gcdB 0 s = 1
-- Mathlib.Analysis.Convex.Basic
convex_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β),
  Convex 𝕜 (Set.Icc r s)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.OplaxTrans.Modification η θ},
  x = y ↔ x.app = y.app
-- Lean.Meta.Match.MatcherInfo
/-- `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
 -/
Lean.Meta.Match.MatcherInfo.discrInfos : Lean.Meta.MatcherInfo → Array Lean.Meta.Match.DiscrInfo
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.isContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K]
  [G.IsLocallyFaithful K], CategoryTheory.CoverPreserving J K G → G.IsContinuous J K
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.vectorMeasure.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ),
  hf.vectorMeasure =
    ⋯.choose +
      if h : ∃ x, IsBot x then MeasureTheory.VectorMeasure.dirac h.choose (Function.rightLim f h.choose - f h.choose)
      else 0
-- Mathlib.Topology.Separation.Connected
/-- A non-trivial connected T1 space has no isolated points.  -/
ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] (x : X),
  (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.NumberTheory.LSeries.Dirichlet
LSeries.one_convolution_eq_zeta_convolution : ∀ {R : Type u_1} [inst : Semiring R] (f : ℕ → R),
  LSeries.convolution 1 f = LSeries.convolution (fun x => ↑(ArithmeticFunction.zeta x)) f
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.trivialization_mem_atlas' : ∀ {B : Type u_2} {F : Type u_3} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F} {E : B → Type u_5}
  {inst_2 : TopologicalSpace (Bundle.TotalSpace F E)} {inst_3 : (b : B) → TopologicalSpace (E b)}
  [self : FiberBundle F E] (b : B), FiberBundle.trivializationAt' b ∈ FiberBundle.trivializationAtlas'
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.injective : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis), Function.Injective ⇑a
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mul_inv : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (t : Matrix.TransvectionStruct n R), t.toMatrix * t.inv.toMatrix = 1
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_comp_map : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A : DiscreteQuotient X} {B B' : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : B ≤ B'),
  DiscreteQuotient.ofLE h ∘ DiscreteQuotient.map f cond = DiscreteQuotient.map f ⋯
-- Lean.Parser.Extension
Lean.Parser.AliasValue.binary.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (p : α → α → α), sizeOf (Lean.Parser.AliasValue.binary p) = 1
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_replicateRow : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateRow ι v‖₊ = ∑ i, ‖v i‖₊
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N₁ N₂ : Submodule R M} {S₁ S₂ : Set M}, N₁ ≤ N₂ → S₁ ⊆ S₂ → N₁.colon S₂ ≤ N₂.colon S₁
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue.0.MeasureTheory.SignedMeasure.eq_singularPart' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
  (t : MeasureTheory.SignedMeasure α) {f : α → ℝ},
  Measurable f →
    MeasureTheory.Integrable f μ →
      MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
        s = t + μ.withDensityᵥ f → t = s.singularPart μ
-- Mathlib.Logic.Function.Basic
Function.invFun_eq : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {b : β}, (∃ a, f a = b) → f (Function.invFun f b) = b
-- Mathlib.RingTheory.PowerSeries.Basic
/-- If a formal power series is invertible, then so is its constant coefficient.  -/
PowerSeries.isUnit_constantCoeff : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), IsUnit φ → IsUnit (PowerSeries.constantCoeff φ)
-- Mathlib.GroupTheory.Complement
Subgroup.instInhabitedRightTransversal.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  Subgroup.instInhabitedRightTransversal = { default := ⟨Set.range Quotient.out, ⋯⟩ }
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.sub_re_self : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddGroup R], a - ↑a.re = a.im
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_div_mul_left : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {c : G₀} (a b : G₀), c ≠ 0 → c * a / (c * b) = a / b
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.ideal_eq_span_pow_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {s : Ideal ℤ_[p]}, s ≠ ⊥ → ∃ n, s = Ideal.span {↑p ^ n}
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.instInhabited : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Preadditive C] → [Inhabited C] → Inhabited (CategoryTheory.Mat_ C)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_eq_right_iff : ∀ {a b : Cardinal.{u_1}}, a + b = b ↔ max Cardinal.aleph0 a ≤ b ∨ a = 0
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instIsTorsionFree : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  [Module.IsTorsionFree R A], Module.IsTorsionFree R ↥S
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_zero : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), M ^ 0 = 1
-- Mathlib.Data.ZMod.QuotientRing
Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero : ∀ {n : ℤ} [NeZero n], Finite (ℤ ⧸ Ideal.span {n})
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn g s → MonotoneOn (fun x => Set.Ioc (f x) (g x)) s
-- Aesop.Forward.State
Aesop.instInhabitedRuleState : Inhabited Aesop.RuleState
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (Std.Slice.toArray xs).extract (lo + 1) hi
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.invOf_exp : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸)
  [inst_3 : Invertible (NormedSpace.exp x)], ⅟(NormedSpace.exp x) = NormedSpace.exp (-x)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonTrace : Lean.FromJson Lean.Lsp.Trace
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_vadd_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] (f : β → γ) (a : α) (s : Set β),
  (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → f '' (a +ᵥ s) = a +ᵥ f '' s
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (s : Set α), AntilipschitzWith K (s.domRestrict f)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_eq_zero : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, w ≤ n → x <<< n = 0#w
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkBEqCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkBEqCached input).aig.decls.size},
  (aig.mkBEqCached input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_iSup : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_2} {f : ι → AddSubmonoid M},
  (iSup f).saturation = ⨆ i, (f i).saturation
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- **Alias** of `Filter.tendsto_atBot_atBot_of_monotone`. -/
Monotone.tendsto_atBot_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → (∀ (b : β), ∃ a, f a ≤ b) → Filter.Tendsto f Filter.atBot Filter.atBot
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_iff_smul_rearrangement`.

---

Two functions antivary iff the rearrangement inequality holds.  -/
Antivary.smul_add_smul_le_smul_add_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β},
  Antivary f g → ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Prod.instMeasurableSpace : {α : Type u_6} → {β : Type u_7} → [m₁ : MeasurableSpace α] → [m₂ : MeasurableSpace β] → MeasurableSpace (α × β)
-- Aesop.Index.Basic
Aesop.IndexingMode.instToFormat : Std.ToFormat Aesop.IndexingMode
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.rank_le_finrank : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [Nontrivial R], LieAlgebra.rank R L ≤ Module.finrank R L
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
OrderedFinpartition.extendEquiv.eq_1 : ∀ (n : ℕ),
  OrderedFinpartition.extendEquiv n =
    { toFun := fun c => c.fst.extend c.snd,
      invFun := fun c =>
        if h : Set.range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Special case of `fderivWithin_neg` for functions `𝕜 → F`, i.e. when the domain `E` is the scalar
field `𝕜` itself. In this case no `UniqueDiffWithinAt 𝕜 s x` hypothesis is needed.  -/
fderivWithin_neg' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {s : Set 𝕜} {f : 𝕜 → F} {x : 𝕜}, fderivWithin 𝕜 (-f) s x = -fderivWithin 𝕜 f s x
-- Lean.Widget.UserWidget
Lean.Widget.addBuiltinModule : Lean.Name → Lean.Widget.Module → IO Unit
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.mem_rootSet_of_mem_rootSpan : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L)
  {α : ↥LieSubalgebra.root}, LieModule.Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan → α ∈ I.rootSet
-- Mathlib.Analysis.Convex.Star
StarConvex.zero_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, StarConvex 𝕜 0 s → ∀ (c : 𝕜), StarConvex 𝕜 0 (c • s)
-- Init.Grind.Util
/-- Marker for grind-solved subproofs in `exact? +grind` suggestions.
When `exact?` uses grind as a discharger, it wraps the proof in this marker
so that the unexpander can replace it with `(by grind)` in the suggestion.
 -/
Lean.Grind.Marker : {α : Sort u} → α → α
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictMono_tendsto_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [FirstCountableTopology α] (x : α),
  ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Iio x))
-- Mathlib.Data.Sign.Defs
/-- Casting out of `SignType` respects composition with functions preserving `0, 1, -1`.  -/
SignType.map_cast' : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α] {β : Type u_2} [inst_3 : One β] [inst_4 : Neg β]
  [inst_5 : Zero β] (f : α → β), f 1 = 1 → f 0 = 0 → f (-1) = -1 → ∀ (s : SignType), f ↑s = ↑s
-- Mathlib.Control.Traversable.Lemmas
Traversable.pure_traverse : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] {α : Type u} (x : t α), traverse pure x = pure x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntryD_eq_getD_minEntry? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {fallback : (a : α) × β a},
  l.minEntryD fallback = l.minEntry?.getD fallback