mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) (h : HomotopicalAlgebra.CofibrantBrownFactorization f) [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence h.i
-- Mathlib.CategoryTheory.Localization.Triangulated
/-- Given a functor `C ⥤ D` from a pretriangulated category, this is the set of
triangles in `D` that are in the essential image of distinguished triangles of `C`.  -/
CategoryTheory.Functor.essImageDistTriang : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.HasShift C ℤ] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                  [CategoryTheory.Pretriangulated C] →
                    [inst_7 : CategoryTheory.HasShift D ℤ] →
                      [L.CommShift ℤ] → Set (CategoryTheory.Pretriangulated.Triangle D)
-- Mathlib.CategoryTheory.Filtered.Small
/-- The factorization through a small filtered category is in fact a factorization, up to natural
isomorphism.  -/
CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringCompInclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            (CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring F).comp
                (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F) ≅
              F
-- Batteries.Data.List.Basic
List.foldrIdx.eq_1 : ∀ {α : Type u} {β : Type v} (f : ℕ → α → β → β) (init : β) (x : ℕ), List.foldrIdx f init [] x = init
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_iff_zeroLocus_ideal : ∀ {R : Type u} [inst : CommSemiring R] (Z : Set (PrimeSpectrum R)), IsClosed Z ↔ ∃ I, Z = PrimeSpectrum.zeroLocus ↑I
-- Mathlib.Topology.Basic
Set.Finite.isOpen_biInter : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X},
  s.Finite → (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋂ i ∈ s, f i)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderDefault : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lift_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  (f : M → α) (h : ∀ (a b : M), ArchimedeanClass.mk a = ArchimedeanClass.mk b → f a = f b) (a : M),
  ArchimedeanClass.lift f h (ArchimedeanClass.mk a) = f a
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.divConst B = ↑(A / B).card / ↑A.card
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructInv_inv : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct),
  I.invStructInv.inv = hom
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `R` has no zero divisors, then multiplication commutes with finsums. See `mul_finsum'` for a
statement assuming finiteness of support.
 -/
mul_finsum : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R),
  r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
Nat.Partition.multipliable_genFun : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R),
  Multipliable fun i => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The `N`-conjugacy classes of splittings  -/
AddGroupExtension.AddConjClasses : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] → {E : Type u_3} → [inst_2 : AddGroup E] → AddGroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (p₁ p₂ p₃ : ℤ) (h₁ : p₁ + n₁ = p₂)
  (h₂ : p₂ + n₂ = p₃), (z₁.comp z₂ h).v p₁ p₃ ⋯ = CategoryTheory.CategoryStruct.comp (z₁.v p₁ p₂ h₁) (z₂.v p₂ p₃ h₂)
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.eq : ∀ {α : Type u_6} [T : TopologicalSpace α] (self : Ctop.Realizer α), self.F.toTopsp = T
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
MonoidHom.map_zpowers : ∀ {G : Type u_1} [inst : Group G] {N : Type u_3} [inst_1 : Group N] (f : G →* N) (x : G),
  Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.le_mul_inv_of_le_mul : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → a ≤ b * c → b ≤ a * c⁻¹
-- Mathlib.Order.Hom.Lattice
orderEmbeddingOfInjective_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : SemilatticeInf α]
  [inst_2 : SemilatticeInf β] (f : F) [inst_3 : InfHomClass F α β] (hf : Function.Injective ⇑f) (a : α),
  (orderEmbeddingOfInjective f hf) a = f a
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.done.injEq : ∀ (result result_1 : String),
  (Std.Http.Internal.UnquoteState.done✝ result = Std.Http.Internal.UnquoteState.done✝ result_1) = (result = result_1)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.funUnique_symm_apply : ∀ (ι : Type u_7) (X : Type u_8) [inst : Unique ι] [inst_1 : TopologicalSpace X],
  ⇑(Homeomorph.funUnique ι X).symm = uniqueElim
-- Lean.Elab.Term.TermElabM
/-- Update the universe level parameter names.  -/
Lean.Elab.Term.setLevelNames : List Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] [inst_6 : NormMulClass R]
  {r : R} (hr : ‖r‖ < 1),
  ↑((PadicInt.continuousAddCharEquiv_of_norm_mul p R).symm ⟨r, hr⟩) = PadicInt.addChar_of_value_at_one r ⋯
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Given a linear map `f : M → N`, we can obtain a short complex `0 → ker(f) → M → N`.  -/
LinearMap.shortComplexKer : {R : Type u} →
  [inst : Ring R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type v} →
            [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (M →ₗ[R] N) → CategoryTheory.ShortComplex (ModuleCat R)
-- Mathlib.Control.LawfulFix
Part.fix_eq_ωSup : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)),
  Part.fix ⇑f = OmegaCompletePartialOrder.ωSup (Part.Fix.approxChain f)
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.top : ∀ {M : Type u_1} [inst : AddZeroClass M], ⊤.AddSaturated
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupMap_apply_coe : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H : AddSubgroup G)
  (x : ↥H.toAddSubmonoid), ↑((f.addSubgroupMap H) x) = f ↑x
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Strips parent projections from `s`. Assumes that the current SubExpr is the same as the one used when delaborating `s`.  -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.stripParentProjections : Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsRight.sInf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)}
  {Q : CategoryTheory.MorphismProperty C}, (∀ W' ∈ W, W'.RespectsRight Q) → (sInf W).RespectsRight Q
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap α β compare} [inst_2 : Inhabited α] {k : α}
  {f : β → β}, compare (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.one_sub_mem : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {t : β},
  t ∈ Set.Icc 0 1 → 1 - t ∈ Set.Icc 0 1
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- Irreducibility of a nonnegative matrix `A` is equivalent to entrywise positivity of some
power: between any two indices `i, j` there exists a positive integer `k` such that the
`(i, j)`-entry of `A ^ k` is strictly positive.  -/
Matrix.isIrreducible_iff_exists_pow_pos : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} [inst_2 : Fintype n]
  [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [inst_6 : DecidableEq n],
  (∀ (i j : n), 0 ≤ A i j) → (A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasLimits : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R], CategoryTheory.Limits.HasLimits (TopModuleCat R)
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_one_left : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime 1 x
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_div_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance (fun ω => X ω / c) Y μ = ProbabilityTheory.covariance X Y μ / c
-- Mathlib.Data.Multiset.ZeroCons
/-- `0 : Multiset α` is the empty set  -/
Multiset.zero : {α : Type u_1} → Multiset α
-- Mathlib.Data.Set.Lattice.Image
Set.sInter_prod_sInter : ∀ {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {T : Set (Set β)},
  S.Nonempty → T.Nonempty → ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_eq_concat_of_lt : ∀ {w : ℕ} {x : BitVec w} {n : ℕ} (hn : n < w), x <<< n = BitVec.cast ⋯ (BitVec.extractLsb' 0 (w - n) x ++ 0#n)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instTopologicalSpace : {R : Type u_3} → {M : Type u_4} → [TopologicalSpace R] → [TopologicalSpace M] → TopologicalSpace (TrivSqZeroExt R M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) {Z : CategoryTheory.Functor C C} (h : Φ.quotient.comp Ψ.r ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom)
      (CategoryTheory.CategoryStruct.comp (Φ.colonπ Ψ) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.subset_smul_finset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → (s ⊆ a • t ↔ a⁻¹ • s ⊆ t)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the constant sequence `1` does not vanish on the right half-plane
`re s > 1`.  -/
LSeries_one_ne_zero_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → LSeries 1 s ≠ 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The ring isomorphism `v.Completion ≃+* ℝ`, when `v` is real, given by the bijection
`v.Completion →+* ℝ`.  -/
NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsReal → v.Completion ≃+* ℝ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivWithinAt_arccos_Iic : ∀ {x : ℝ}, x ≠ 1 → HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Iic x) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGE!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited ((a : α) × β a)],
          Std.DTreeMap.Internal.Impl.getEntryGE! k t₁ = Std.DTreeMap.Internal.Impl.getEntryGE! k t₂
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_ext : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {f g : M ⟶ N},
  SemimoduleCat.Hom.hom f = SemimoduleCat.Hom.hom g → f = g
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_sub : ∀ (a b : BitVec 16), Int16.ofBitVec (a - b) = Int16.ofBitVec a - Int16.ofBitVec b
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_union_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.Groupoid.Discrete
CategoryTheory.instGroupoidDiscrete : {C : Type u_1} → CategoryTheory.Groupoid (CategoryTheory.Discrete C)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : (Std.DHashMap.Internal.AssocList α fun x => β) → Sort u_3) →
      (x : Std.DHashMap.Internal.AssocList α fun x => β) →
        (Unit → motive Std.DHashMap.Internal.AssocList.nil) →
          ((k : α) →
              (v : β) →
                (es : Std.DHashMap.Internal.AssocList α fun x => β) →
                  motive (Std.DHashMap.Internal.AssocList.cons k v es)) →
            motive x
-- Mathlib.Algebra.Group.Fin.Basic
/-- Variant of `Fin.intCast_def` with `Nat.cast` on the RHS.  -/
Fin.intCast_def' : ∀ {n : ℕ} [inst : NeZero n] (x : ℤ), ↑x = if 0 ≤ x then ↑x.natAbs else -↑x.natAbs
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, compute the trailing
coefficient of `f` in terms of `divisor f U` and `g x`.
 -/
MeromorphicOn.meromorphicTrailingCoeffAt_extract_zeros_poles : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {x : 𝕜} {f g : 𝕜 → E} {D : 𝕜 → ℤ},
  Function.HasFiniteSupport D →
    x ∈ U →
      AccPt x (Filter.principal U) →
        MeromorphicAt f x →
          AnalyticAt 𝕜 g x →
            g x ≠ 0 →
              f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x => x - u) ^ D u) • g →
                meromorphicTrailingCoeffAt f x = (∏ᶠ (u : 𝕜), (x - u) ^ Function.update D x 0 u) • g x
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_pos : ∀ {α : Type u} {s : Set α} [inst : MetricSpace α], s.Nontrivial → Bornology.IsBounded s → 0 < Metric.diam s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey? = some t.minKey!
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.neg_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), ∀ x ∈ A, -x ∈ A
-- Init.Data.SInt.Lemmas
instAssociativeInt8HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_union : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] {s t : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
  (f : ((i : δ) → X i) → ENNReal), Measurable f → Disjoint s t → ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ
-- Mathlib.LinearAlgebra.Isomorphisms
Submodule.quotientQuotientEquivQuotientAux_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M)
  (h : S ≤ T) (x : M ⧸ S),
  (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk x) = (S.mapQ T LinearMap.id h) x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.inv.eq_1 : ∀ (t : Tactic.ComputeAsymptotics.Monomial), t.inv = { coef := t.coef⁻¹, unit := t.unit.inv }
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map `fun y ↦ ⟪x, y⟫`.  -/
ProperCone.innerDual_singleton : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E] (x : E),
  ProperCone.innerDual {x} = ProperCone.comap ((innerSL ℝ) x) (ProperCone.positive ℝ ℝ)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.coe_range : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (φ : F), ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold_le_size_of_le_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len x : ℕ} (aig : Std.Sat.AIG α) (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func],
  x ≤ aig.decls.size → x ≤ (Std.Sat.AIG.RefVec.fold aig vec func).aig.decls.size
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.coe_id : ∀ (V : SemiNormedGrp), ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id V)) = id
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_map : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : MeasurableSpace Y] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G]
  (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) {φ : X → Y},
  (μ.map φ).transpose B = (μ.transpose B).map φ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_contra' : ∀ {w : ℕ} (a : BitVec w), ~~~a &&& a = 0#w
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.singleton_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α], Function.Injective fun x => {x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.preΨ₄_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 2 ≠ 0 → W.preΨ₄ ≠ 0
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.brecOn.go : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} →
      {motive : CommRingCat.Colimits.Prequotient F → Sort u} →
        (t : CommRingCat.Colimits.Prequotient F) →
          ((t : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Prequotient.below t → motive t) →
            motive t ×' CommRingCat.Colimits.Prequotient.below t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.size_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.toLinearMap_convPow : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (f : WithConv (C →ₐ[R] A)) (n : ℕ),
  WithConv.toConv (f ^ n).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap ^ n
-- Init.Data.List.Lemmas
List.map_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {b : β},
  List.map f l = List.replicate l.length b ↔ ∀ x ∈ l, f x = b
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.mk.sizeOf_spec : ∀ (line : Std.Format) (column : ℕ) (tags : List (ℕ × Std.Format)),
  sizeOf { line := line, column := column, tags := tags } = 1 + sizeOf line + sizeOf column + sizeOf tags
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Membership in `S p i` is strict monotonicity of the bordered word.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.mem_S_iff : ∀ {n p : ℕ} {i : Fin n} {α : Fin p → Fin n}, α ∈ BirdDet.S✝ p i ↔ StrictMono (Fin.cons i α)
-- Mathlib.Order.SupIndep
/-- An independent set of elements in a complete lattice is one in which every element is disjoint
from the `Sup` of the rest.  -/
sSupIndep : {α : Type u_1} → [CompleteLattice α] → Set α → Prop
-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.equiv_functor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C} (θ : X ⟶ Y),
  CategoryTheory.Functor.equiv.functor.map θ = θ.app { as := PUnit.unit }
-- Aesop.Index.Forward
/-- Get forward rule matches for the constant forward rules (i.e., those with no
premises and no rule pattern). Accordingly, the returned matches contain no
hypotheses.  -/
Aesop.ForwardIndex.getConstRuleMatches : Aesop.ForwardIndex → Array Aesop.ForwardRuleMatch
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (P.comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toPlus P) F)
      (CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom h) =
    CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) h
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTreeTransform.default : Lean.Language.SnapshotTreeTransform
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_neg : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F)
  (x : ↥f.domain), ↑f (-x) = -↑f x