mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Inseparable
stableUnderSpecialization_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], StableUnderSpecialization ∅
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.topEquiv_apply : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (self : { x // x ∈ Set.univ }), (AffineSubspace.topEquiv k V P) self = ↑self
-- Init.Data.SInt.Lemmas
Int8.add_assoc : ∀ (a b c : Int8), a + b + c = a + (b + c)
-- Mathlib.RingTheory.RingHom.LocallyStandardSmooth
/-- Any smooth ring homomorphism is locally standard smooth.  -/
RingHom.Smooth.locally_isStandardSmooth : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Smooth → RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth) f
-- Batteries.Data.Nat.Basic
/-- Diagonal recursor for `Nat`
 -/
Nat.recDiagOn : {motive : ℕ → ℕ → Sort u_1} →
  (m n : ℕ) →
    motive 0 0 →
      ((n : ℕ) → motive 0 n → motive 0 (n + 1)) →
        ((m : ℕ) → motive m 0 → motive (m + 1) 0) → ((m n : ℕ) → motive m n → motive (m + 1) (n + 1)) → motive m n
-- Mathlib.Util.PrintSorries
/-- - `#print sorries` prints all sorries that the current module depends on.
- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on.
- `#print sorries in CMD` prints all the sorries in declarations added by the command.

Displayed sorries are hoverable and support "go to definition".
 -/
Mathlib.PrintSorries.printSorriesStx : Lean.ParserDescr
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.mem_closedBall_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] {a : M} {c : FiniteArchimedeanClass M},
  a ∈ FiniteArchimedeanClass.closedBall K c ↔ ∀ (h : a ≠ 0), c ≤ FiniteArchimedeanClass.mk a h
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- We can always derive `PreservesFiniteColimits C`
by showing that we are preserving colimits at an arbitrary universe.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  (∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J),
      CategoryTheory.Limits.PreservesColimitsOfShape J F) →
    CategoryTheory.Limits.PreservesFiniteColimits F
-- Init.Data.Iterators.Consumers.Access
_private.Init.Data.Iterators.Consumers.Access.0.Std.Iter.atIdxSlow?.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out property
-- Mathlib.Order.Filter.Basic
Filter.mem_principal_self : ∀ {α : Type u} (s : Set α), s ∈ Filter.principal s
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_rii : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [inst_4 : Std.PRange.Least? α] [inst_5 : Std.PRange.UpwardEnumerable α] [inst_6 : Std.Rxi.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] {xs : Std.Rii α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Data.Set.Prod
Set.prod_sdiff_prod : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.toIsSubDPIdeal : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J : hI.SubDPIdeal),
  hI.IsSubDPIdeal J.carrier
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z),
  (α ≪≫ β).symm = β.symm ≪≫ α.symm
-- Lean.Meta.Tactic.Grind.Util
Lean.MVarId.transformTarget : Lean.MVarId → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.MVarId
-- Mathlib.Data.Set.Sups
Set.image_subset_infs_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α} {b : α}, b ∈ t → (fun a => a ⊓ b) '' s ⊆ s ⊼ t
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instHashablePosition.hash : Lean.Lsp.Position → UInt64
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t₁.Equiv t₂ → ∀ (k : α) (f : Option β → Option β), (t₁.alter k f).Equiv (t₂.alter k f)
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Seminormed commutative ring structure on the product of finitely many seminormed commutative
rings, using the sup norm.  -/
Pi.seminormedCommRing : {ι : Type u_3} →
  {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedCommRing (R i)] → SeminormedCommRing ((i : ι) → R i)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.lazy : {α β : Type} → β → Lean.Widget.StrictOrLazy α β
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_univ : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.Measure.count Set.univ = ↑(ENat.card α)
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the natural transformation
`H ⟶ F` is epic at `X` iff the image of the unit of the adjunction `F ⊣ G` under `H` is.  -/
CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_app : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  {X : C}, CategoryTheory.Epi (t.rightToLeft.app X) ↔ CategoryTheory.Epi (H.map (t.adj₁.unit.app X))
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- In the setting of `MeromorphicOn.extract_zeros_poles`, compute the log of the
norm of the trailing coefficient of `f` in terms of `divisor f U` and `g x`.
 -/
MeromorphicOn.log_norm_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 →
                Real.log ‖meromorphicTrailingCoeffAt f x‖ = ∑ᶠ (u : 𝕜), ↑(D u) * Real.log ‖x - u‖ + Real.log ‖g x‖
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a : α} {fallback : β}, m.contains a = false → Std.DHashMap.Raw.Const.getD m a fallback = fallback
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_prepartition_boxes_iff : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] [inst_1 : Fintype ι] {B I : BoxIntegral.Box ι},
  I ∈ (BoxIntegral.unitPartition.prepartition n B).boxes ↔
    ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, BoxIntegral.unitPartition.box n ν = I
-- Lean.Message
Lean.instBEqMessageSeverity.beq : Lean.MessageSeverity → Lean.MessageSeverity → Bool
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_pi_eq_zero : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {j : ι},
  Monoid.exponent (M j) = 0 → Monoid.exponent ((i : ι) → M i) = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_max?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.max?.isSome = !t.isEmpty
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: The (`r`-power of the) `L^r` norm of the product of two functions is
bounded by the product of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q`, and `r`
form a `Real.HolderTriple`.  -/
NNReal.Lr_rpow_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q r : ℝ},
  p.HolderTriple q r → ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.mem_add : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
  Projectivization.Subspace.spanCarrier S (Projectivization.mk K v hv) →
    Projectivization.Subspace.spanCarrier S (Projectivization.mk K w hw) →
      Projectivization.Subspace.spanCarrier S (Projectivization.mk K (v + w) hvw)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.pointwise_central_scalar : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K]
  [inst_3 : MulSemiringAction Gᵐᵒᵖ K] [IsCentralScalar G K], IsCentralScalar G (ValuationSubring K)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sub_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv},
  f.LimZero → g.LimZero → (f - g).LimZero
-- Std.Time.Format.Modifier
Std.Time.Modifier.A.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.A presentation = Std.Time.Modifier.A presentation_1 → presentation = presentation_1
-- Batteries.Recycling.RBTree.Depth
/-- `O(n)`. `depth t` is the maximum number of nodes on any path to a leaf.
It is an upper bound on most tree operations.
 -/
RBTree.RBNode.depth : {α : Type u_1} → RBTree.RBNode α → ℕ
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleResponse.mk.sizeOf_spec : ∀ (queryResults : Array Lean.Lsp.LeanQueriedModule), sizeOf { queryResults := queryResults } = 1 + sizeOf queryResults
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.equiv_tmul : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (s : S) (m : M),
  h.equiv (s ⊗ₜ[R] m) = s • f m
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then `e₁` uniquely determines `e₂`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityUnit_unique_right : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ e₂' : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂' → e₂ = e₂'
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `filter` which can be used in the absence of balance
information but still assumes the preconditions of `filter`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.filter! : {α : Type u} →
  {β : α → Type v} → [Ord α] → ((a : α) → β a → Bool) → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_zmod_p : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Polynomial.dickson 1 1 p = Polynomial.X ^ p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_clz : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVUnOp.clz.eval = BitVec.clz
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (i : ℕ), p.reverse.getVert i = p.getVert (p.length - i)
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.eq_def : ∀ (a : Array Lean.SyntaxNodeKind) (x : Std.HashSet Lean.Syntax.Range) (x_1 : Lean.Syntax),
  Mathlib.Linter.Style.Whitespace.getUnlintedRanges✝ a x x_1 =
    match x, x_1 with
    | curr, s@h:(Lean.Syntax.node info kind args) =>
      have new :=
        Array.foldl (fun x1 x2 => x1.union (Mathlib.Linter.Style.Whitespace.getUnlintedRanges✝ a curr x2)) curr args;
      if a.contains kind = true then new.insert (s.getRange?.getD default) else new
    | curr, Lean.Syntax.atom info "where" =>
      match Lean.SourceInfo.getRangeWithTrailing? false info with
      | some trail => curr.insert trail
      | x => curr
    | curr, x => curr
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebraClass.subtype_injective : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SetLike S A] [inst_4 : NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A]
  (s : S), Function.Injective ⇑(NonUnitalSubalgebraClass.subtype s)
-- Mathlib.Algebra.Notation.Prod
Prod.pow_mk : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E] (a : α) (b : β) (c : E),
  (a, b) ^ c = (a ^ c, b ^ c)
-- Init.Prelude
/-- The current recursion depth.  -/
Lean.Macro.Context.currRecDepth : Lean.Macro.Context → ℕ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.matched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos →
    String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l →
      String.Slice.Pattern.Model.IsValidRevSearchFrom pat endPos
        (String.Slice.Pattern.SearchStep.matched startPos endPos :: l)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.IsStableUnderPostcomp.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C},
  (∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z),
      r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)) →
    CategoryTheory.HomRel.IsStableUnderPostcomp r
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- [Kerodon Tag 02MK](https://kerodon.net/tag/02MK) -/
SSet.Nonsingular.of_mono : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] [Y.Nonsingular], X.Nonsingular
-- Mathlib.Order.Filter.Map
Filter.inf_principal_eq_bot_iff_comap : ∀ {α : Type u_1} {F : Filter α} {s : Set α}, F ⊓ Filter.principal s = ⊥ ↔ Filter.comap Subtype.val F = ⊥
-- Mathlib.Probability.Moments.ComplexMGF
/-- `complexMGF X μ` is analytic on the vertical strip
`{z | z.re ∈ interior (integrableExpSet X μ)}`.  -/
ProbabilityTheory.analyticOn_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOn ℂ (ProbabilityTheory.complexMGF X μ) {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}
-- Init.Data.SInt.Lemmas
Int16.mul_assoc : ∀ (a b c : Int16), a * b * c = a * (b * c)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.comapSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (f : G ≃* H),
  f.comapSubgroup =
    { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Init.Control.Lawful.Instances
Option.elim.eq_1 : ∀ {α : Type u_1} {β : Sort u_2} (x : β) (x_1 : α → β) (x_3 : α), (some x_3).elim x x_1 = x_1 x_3
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
either isomorphic (and order-isomorphic) to `ℤᵐ⁰`, or is densely ordered.  -/
LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered : ∀ (G : Type u_2) [inst : LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G],
  Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.of_smul_of : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M] {i : ιA} {j : ιB}
  (x : A i) (y : M j),
  (DirectSum.of A i) x • (DirectSum.of M j) y = (DirectSum.of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Continuous.continuousLinearMapCoprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G},
  Continuous f → Continuous g → Continuous fun x => (f x).coprod (g x)
-- Mathlib.Data.Set.Insert
Set.pair_comm : ∀ {α : Type u_1} (a b : α), {a, b} = {b, a}
-- Mathlib.GroupTheory.Generators
/-- If two homomorphisms coincide on the elements of a generating family, then they are equal.  -/
Group.Generators.hom_ext : ∀ {G : Type u_1} {ι : Type u_3} [inst : Group G] (P : Group.Generators G ι) {M : Type u_5} [inst_1 : Monoid M]
  (f g : G →* M), (∀ (i : ι), f (P.val i) = g (P.val i)) → f = g
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_mulVec_eq_vec : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A : Matrix n n α}
  [Invertible A] {u v : n → α}, u = A.mulVec v → A⁻¹.mulVec u = v
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.coconeOfCoconeForget_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))),
  (TopCat.coconeOfCoconeForget c).pt = TopCat.of (TopCat.coconePtOfCoconeForget c)
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearIsometry.extend_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {V : Type u_7} [inst_1 : NormedAddCommGroup V] [inst_2 : InnerProductSpace 𝕜 V]
  [inst_3 : FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) (s : ↥S), L.extend ↑s = L s
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.mem_unop : ∀ {G : Type u_2} [inst : AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ}, x ∈ S.unop ↔ AddOpposite.op x ∈ S
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ AntivaryOn f (g ∘ ⇑σ) ↑s)
-- Mathlib.Order.Booleanisation
Booleanisation.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Booleanisation α)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.mk.inj : ∀ {map map_1 : Lean.SMap Lean.Name Lean.Meta.MatcherInfo}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_pred_left_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  b < a → Set.Ioo (Order.pred b) a = insert b (Set.Ioo b a)
-- Init.Data.Int.Cooper
/-- Right Cooper resolution of an upper and lower bound with divisibility constraint.
 -/
Int.cooper_resolution_dvd_right : ∀ {a b c d s p q : ℤ},
  0 < a →
    0 < b →
      0 < d →
        ((∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) ↔
          ∃ k,
            0 ≤ k ∧
              k < ↑(b.lcm (b * d / ↑((b * d).gcd c))) ∧
                a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * d ∣ -c * k + c * q + b * s)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mapsTo : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.MapsTo (↑e) e.source e.target
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.eq_append_of_dropSuffix?_char_eq_some : ∀ {c : Char} {s : String} {res : String.Slice}, s.dropSuffix? c = some res → s = res.copy ++ String.singleton c
-- Mathlib.Topology.Algebra.Support
/-- A function `f` *has compact multiplicative support* or is *compactly supported* if the closure
of the multiplicative support of `f` is compact. In a T₂ space this is equivalent to `f` being equal
to `1` outside a compact set.  -/
HasCompactMulSupport : {α : Type u_2} → {β : Type u_4} → [TopologicalSpace α] → [One β] → (α → β) → Prop
-- Mathlib.Algebra.Opposites
MulOpposite.unop_eq_one_iff : ∀ {α : Type u_1} [inst : One α] (a : αᵐᵒᵖ), MulOpposite.unop a = 1 ↔ a = 1
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0),
  MvPowerSeries.expand p hp = MvPowerSeries.substAlgHom ⋯
-- Init.Data.Array.Attach
Array.count_attachWith : ∀ {α : Type u_1} [inst : BEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : { x // p x }},
  Array.count a (xs.attachWith p H) = Array.count (↑a) xs
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  P f →
    ∀ [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f],
      CategoryTheory.Presieve.singleton f ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings Y