mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_mapWithPostcondition : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o]
  {it : Std.Iter β} {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        g __do_lift acc ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.mapWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Lean.Data.JsonRpc
/-- The client has canceled a request and a server as detected the cancel.  -/
Lean.JsonRpc.ErrorCode.requestCancelled : Lean.JsonRpc.ErrorCode
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
FormalMultilinearSeries.restrictScalars.congr_simp : ∀ (𝕜 : Type u) {𝕜' : Type u'} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : Semiring 𝕜'] [inst_12 : SMul 𝕜 𝕜'] [inst_13 : Module 𝕜' E]
  [inst_14 : ContinuousConstSMul 𝕜' E] [inst_15 : IsScalarTower 𝕜 𝕜' E] [inst_16 : Module 𝕜' F]
  [inst_17 : ContinuousConstSMul 𝕜' F] [inst_18 : IsScalarTower 𝕜 𝕜' F] (p p_1 : FormalMultilinearSeries 𝕜' E F),
  p = p_1 → ∀ (n : ℕ), FormalMultilinearSeries.restrictScalars 𝕜 p n = FormalMultilinearSeries.restrictScalars 𝕜 p_1 n
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates limits, then `F.leftOp : Cᵒᵖ ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T),
  NonUnitalStarSubalgebra.inclusion h = NonUnitalStarSubalgebra.inclusion h
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.trans : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WSameSide x y → s.WSameSide y z → y ∉ s → s.WSameSide x z
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
Std.Sat.AIG.RefVec.fold.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (vec vec_1 : aig.RefVec len),
  vec = vec_1 →
    ∀ (func func_1 : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) (e_func : func = func_1)
      [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func],
      Std.Sat.AIG.RefVec.fold aig vec func = Std.Sat.AIG.RefVec.fold aig vec_1 func_1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomologicalComplex.isIso_quotient_map_iff_homotopyEquivalences : ∀ {ι : Type u_3} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {K L : HomologicalComplex V c} (f : K ⟶ L),
  CategoryTheory.IsIso ((HomotopyCategory.quotient V c).map f) ↔ HomologicalComplex.homotopyEquivalences V c f
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink.mk : Lean.StrLit → Lean.Doc.ElabLink✝
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_top`. -/
Topology.CWComplex.skeletonLT_top : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ↑(Topology.RelCWComplex.skeletonLT C ⊤) = C
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_insert : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Generates.eq_1 : ∀ {T : Type u_1} (g : ContextFreeGrammar T) (s : List (Symbol T g.NT)),
  g.Generates s = g.Derives [Symbol.nonterminal g.initial] s
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- If `f` is smooth of relative dimension `n` and `g` is smooth of relative dimension
`m`, then `f ≫ g` is smooth of relative dimension `n + m`.  -/
AlgebraicGeometry.smoothOfRelativeDimension_comp : ∀ (n m : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z)
  [hf : AlgebraicGeometry.SmoothOfRelativeDimension n f] [hg : AlgebraicGeometry.SmoothOfRelativeDimension m g],
  AlgebraicGeometry.SmoothOfRelativeDimension (n + m) (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_intCast_mul : ∀ {x : ℝ} (m : ℤ), Irrational (↑m * x) → Irrational x
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.of_isPrincipalIdealRing : ∀ (R : Type u) [inst : Semiring R] [IsPrincipalIdealRing R], IsBezout R
-- Mathlib.Algebra.Group.PUnit
PUnit.addCommGroup : AddCommGroup PUnit.{u_1 + 1}
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.norm_eq_max_natAbs : ∀ (x : Fin 2 → ℤ), ‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.ext : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [IsScalarTower R A P] {g h : TensorProduct R M N →ₗ[A] P},
  (∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) → g = h
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.LinearAlgebra.PiTensorProduct.Basis
Basis.piTensorProduct_repr_tprod_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  (b : (i : ι) → Module.Basis (κ i) R (M i)) (x : (i : ι) → M i) (p : (i : ι) → κ i),
  ((Basis.piTensorProduct b).repr ((PiTensorProduct.tprod R) x)) p = ∏ i, ((b i).repr (x i)) (p i)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), f.Smooth = Algebra.Smooth R S
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.g_ne_h : ∀ {A B : GrpCat} (f : A ⟶ B),
  ∀ x ∉ (GrpCat.Hom.hom f).range, GrpCat.SurjectiveOfEpiAuxs.g f ≠ GrpCat.SurjectiveOfEpiAuxs.h f
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_mul_right_of_mem : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S ↑K) {g k : G} (h : k ∈ K),
  hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * ⟨k, h⟩)
-- Mathlib.LinearAlgebra.Reflection
Module.bijOn_reflection_of_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} {Φ : Set M} (h : f x = 2),
  Set.MapsTo (⇑(Module.reflection h)) Φ Φ → Set.BijOn (⇑(Module.reflection h)) Φ Φ
-- Init.Data.BitVec.Basic
/-- Signed T-division (using the truncating rounding convention) for bitvectors. This function obeys the
Lean convention that division by zero returns zero.

Examples:
* `(7#4).sdiv 2 = 3#4`
* `(-8#4).sdiv 2 = -4#4`
* `(5#4).sdiv -2 = -2#4`
* `(-7#4).sdiv (-2) = 3#4`
 -/
BitVec.sdiv : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃.app T = T.mor₂
-- Mathlib.Algebra.Lie.Semisimple.Basic
/-- An abelian Lie algebra with trivial radical is trivial.  -/
LieAlgebra.subsingleton_of_hasTrivialRadical_lie_abelian : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.HasTrivialRadical R L] [h : IsLieAbelian L], Subsingleton L
-- Mathlib.Algebra.Order.Floor.Defs
FloorSemiring.mk : {α : Type u_4} →
  [inst : Semiring α] →
    [inst_1 : PartialOrder α] →
      (floor ceil : α → ℕ) →
        (∀ {a : α}, a < 0 → floor a = 0) →
          (∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor a ↔ ↑n ≤ a)) → GaloisConnection ceil Nat.cast → FloorSemiring α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] {n : ℕ} {m : Fin n → E} {f : SchwartzMap E F} {x : E},
  (LineDeriv.iteratedLineDerivOp m f) x = (iteratedFDeriv ℝ n (⇑f) x) m
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a ⊆ Set.Iic a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.HashMap.Raw α β) (e_m : m = m_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSectionsOn.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → Set β} {s : Set α},
  HasOpenLowerSectionsOn f s → HasOpenLowerSectionsOn g s → HasOpenLowerSectionsOn (fun x => f x ∩ g x) s
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_left : ∀ (n k : ℕ), 0 < k → (n + 1).choose k = n.choose (k - 1) + n.choose k
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_commonNeighbors_lt_card_verts : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v w : V),
  Fintype.card ↑(G.commonNeighbors v w) < Fintype.card V
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub : ∀ (p : ℝ), Real.binEntropy p = p.negMulLog + (1 - p).negMulLog
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂' : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (pq' : κ) {i₁ i₂ : ι},
  i₁ = data.i₁ pq' → i₂ = data.i₂ pq' → i₁ ≤ i₂
-- Mathlib.Order.RelSeries
RelSeries.coe_ofLE : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (h : r ⊆ s), (x.ofLE h).toFun = x.toFun
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.Disjoint.cycleOf_mul_distrib : ∀ {α : Type u_2} {f g : Equiv.Perm α} [inst : DecidableRel f.SameCycle] [inst_1 : DecidableRel g.SameCycle]
  [inst_2 : DecidableRel (f * g).SameCycle], f.Disjoint g → ∀ (x : α), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
-- Mathlib.Logic.Function.ULift
ULift.down_injective : ∀ {α : Type u_1}, Function.Injective ULift.down
-- Mathlib.Algebra.Notation.Support
Function.support_binop_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
  (op : M → N → P),
  op 0 0 = 0 →
    ∀ (f : ι → M) (g : ι → N), (Function.support fun x => op (f x) (g x)) ⊆ Function.support f ∪ Function.support g
-- Mathlib.FieldTheory.CardinalEmb
/-- The functor on `WithTop ι` given by embeddings of `E⟮<i⟯` into `Ē`  -/
Field.Emb.Cardinal.embFunctor : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              ⦃i j : WithTop (Module.rank F E).ord.ToType⦄ →
                i ≤ j →
                  (↥(Field.Emb.Cardinal.filtration j) →ₐ[F] AlgebraicClosure E) →
                    ↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulLeft_one : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A], LinearMap.mulLeft R 1 = LinearMap.id
-- Init.Data.BitVec.Bitblast
BitVec.carry_succ_one : ∀ {w : ℕ} (i : ℕ) (x : BitVec w), 0 < w → BitVec.carry (i + 1) x (1#w) false = decide (∀ j ≤ i, x.getLsbD j = true)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateL_node : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (sz : ℕ) (m : Ordnode α) (y : α) (r : Ordnode α),
  l.rotateL x (Ordnode.node sz m y r) = if m.size < Ordnode.ratio * r.size then l.node3L x m y r else l.node4L x m y r
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.instIsEquivalenceOppositeUnopUnop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.unopUnop C).IsEquivalence
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instMonoICycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  CategoryTheory.Mono (X.iCycles f g n)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The coequalizer of a morphism with itself is isomorphic to the target.  -/
CategoryTheory.Limits.coequalizer.isoTargetOfSelf : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (f : X ⟶ Y) → CategoryTheory.Limits.coequalizer f f ≅ Y
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.mem_inertia : ∀ {M : Type u_6} [inst : AddGroup M] {I : AddSubgroup M} {G : Type u_7} [inst_1 : Group G] [inst_2 : MulAction G M]
  {σ : G}, σ ∈ I.inertia G ↔ ∀ (x : M), σ • x - x ∈ I
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.sieve_mem : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.Functor.IsDenseSubsite J₀ J F] {X : C}
  (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀} (f : F.obj X₀ ⟶ X), data.sieve f ∈ J₀ X₀
-- Mathlib.CategoryTheory.Square
CategoryTheory.NatTrans.mapSquare_app_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C),
  ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₁ = τ.app sq.X₁
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The unit vector in the new dimension  -/
CliffordAlgebra.EquivEven.e0 : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q)
-- Init.Data.SInt.Basic
instShiftRightInt8 : ShiftRight Int8
-- Mathlib.RingTheory.Ideal.Operations
Submodule.coe_mapAlgHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (p : Submodule R A),
  ↑((Submodule.mapAlgHom f) p) = ⇑f '' ↑p
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.instFaithfulProdCurry : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E], CategoryTheory.Functor.curry.Faithful
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpOptions.toJson : Lean.Lsp.SignatureHelpOptions → Lean.Json
-- Mathlib.Data.Int.Cast.Lemmas
map_intCast : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : NonAssocRing α] [inst_1 : NonAssocRing β]
  [inst_2 : FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ), f ↑n = ↑n
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The characterization of weak convergence of finite measures by the usual (defining)
condition that the integrals of every continuous bounded function are continuous.  -/
MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_integral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.FiniteMeasure Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, ℝ)), Continuous fun x => ∫ (ω : Ω), f ω ∂↑(μs x)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
DegLex.forall_iff : ∀ {α : Type u_1} {p : DegLex α → Prop}, (∀ (a : DegLex α), p a) ↔ ∀ (a : α), p (toDegLex a)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, for all `z : N`
we have that if `x : M, y ∈ S` are such that `z + f y = f x`, then `f x - f y = z`.  -/
AddSubmonoid.LocalizationMap.mk'_sec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z : N), f.mk' (f.sec z).1 (f.sec z).2 = z
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrixAux.eq_1 : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} (b : n → M₁), LinearMap.BilinForm.toMatrixAux b = LinearMap.toMatrix₂Aux R₁ b b
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instOne : {α : Type u} → One (FreeGroup α)
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivAt_finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : (i : Fin n.succ) → F' i},
  HasDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔ HasDerivAt φ (φ' 0) x ∧ HasDerivAt φs (fun i => φ' i.succ) x
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.toAddGroupSeminorm : {G : Type u_6} → [inst : AddGroup G] → AddGroupNorm G → AddGroupSeminorm G
-- Init.Data.Option.List
Option.head?_toList : ∀ {α : Type u_1} {o : Option α}, o.toList.head? = o
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instSMulCommClass : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : CommSemiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : Module A M], SMulCommClass R S (TensorAlgebra A M)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_5.splitter : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {x y : (CategoryTheory.WithInitial C)ᵒᵖ} →
      (motive : (x ⟶ y) → Sort u_3) →
        (x_1 : x ⟶ y) → ((f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)) → motive x_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_int_mul_two_pi_sub_pi : ∀ (n : ℤ), Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_eq_get!_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {a : α}, Std.DHashMap.Internal.Raw₀.Const.get! m a = (Std.DHashMap.Internal.Raw₀.Const.get? m a).get!
-- Mathlib.Data.Rel
SetRel.preimage_empty_left : ∀ {α : Type u_1} {β : Type u_2} (t : Set β), ∅.preimage t = ∅
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_id : ∀ {𝕜 : 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] {s : Set M} {x : M},
  UniqueMDiffAt[s] x → mfderiv[s] id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_iff_existsUnique_mul_inv_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! t, g * (↑t)⁻¹ ∈ S
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roo : ∀ {m n i fallback : ℕ}, (m<...n).toList.getD i fallback = if i < n - (m + 1) then m + 1 + i else fallback
-- Init.LawfulBEqTactics
DerivingHelpers.tacticDeriving_ReflEq_tactic : Lean.ParserDescr
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- See `expGrowthInf_mul_le'` for a version with swapped argument `u` and `v`.  -/
ExpGrowth.expGrowthInf_mul_le : ∀ {u v : ℕ → ENNReal},
  ExpGrowth.expGrowthSup u ≠ ⊥ ∨ ExpGrowth.expGrowthInf v ≠ ⊤ →
    ExpGrowth.expGrowthSup u ≠ ⊤ ∨ ExpGrowth.expGrowthInf v ≠ ⊥ →
      ExpGrowth.expGrowthInf (u * v) ≤ ExpGrowth.expGrowthSup u + ExpGrowth.expGrowthInf v
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_succ : ∀ (n : ℕ), catalan (n + 1) = ∑ i, catalan ↑i * catalan (n - ↑i)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_swap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V W s = -VectorField.mlieBracketWithin I W V s
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the intermediate objects in the factorizations  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      W₁.FunctorialFactorizationData W₂ → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.RingTheory.Finiteness.Basic
LinearMap.finite_iff_of_bijective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_7}
  {P : Type u_6} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [RingHomSurjective σ] (f : M →ₛₗ[σ] P), Function.Bijective ⇑f → (Module.Finite R M ↔ Module.Finite S P)