mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.eraseManyEntries.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.eraseManyEntries l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, snd⟩ =>
              have r := ⟨(↑r).erase a, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α}, P m'' → P (m''.erase a)) → P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The tangent space at the identity of a Lie group is a Lie ring, for the bracket
given by the Lie bracket of invariant vector fields.  -/
instLieRingGroupLieAlgebra : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Group G] →
                        [LieGroup I (minSmoothness 𝕜 3) G] → [CompleteSpace E] → LieRing (GroupLieAlgebra I G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.toCostructuredArrow_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) {X Y : (CategoryTheory.StructuredArrow d F)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.StructuredArrow.toCostructuredArrow F d).map f =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f.unop).op ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (v : β k), (t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β k}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toLinearEquiv_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ↑e.toLinearEquiv = ↑↑e
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g],
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F) →
    CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F
-- Mathlib.RingTheory.Ideal.Operations
Submodule.coe_span_smul : ∀ {R' : Type u_1} {M' : Type u_2} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M'] [inst_2 : Module R' M']
  (s : Set R') (N : Submodule R' M'), ↑(Ideal.span s) • N = s • N
-- Init.Data.String.Substring
/-- Checks whether the Boolean predicate `p` returns `true` for any character in a substring.

Short-circuits at the first character for which `p` returns `true`.
 -/
Substring.Raw.any : Substring.Raw → (Char → Bool) → Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.TreeMap.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x t[x]).get!
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂ : ∀ {α : Type u_2} {γ : Type u_4} {β : α → Type u_6} [inst : (x : α) → OmegaCompletePartialOrder (β x)]
  [inst_1 : OmegaCompletePartialOrder γ] {f : γ → (x : α) → β x},
  OmegaCompletePartialOrder.ωScottContinuous f ↔ ∀ (a : α), OmegaCompletePartialOrder.ωScottContinuous fun x => f x a
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqArg : BEq Lean.IR.Arg
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.head'_eq_head : ∀ {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ), PFunctor.Approx.head' (x.approx (n + 1)) = x.head
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_natCast : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ),
  WittVector.truncateFun n ↑m = ↑m
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP.go_ne_nil : ∀ {α : Type u_1} (p : α → Bool) (xs acc : List α), List.splitOnPPrepend p xs acc ≠ []
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α} {x : β}, x ∈ a • t ↔ ∃ y ∈ t, a • y = x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.mk : {σ : Type} → Lean.Syntax → Array Lean.Elab.Term.Do.Var → Lean.Syntax → σ → Lean.Elab.Term.Do.Alt σ
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.iInf.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} [inst : Finite β] (f f_1 : β → L.BoundedFormula α n),
  f = f_1 → FirstOrder.Language.BoundedFormula.iInf f = FirstOrder.Language.BoundedFormula.iInf f_1
-- Mathlib.Topology.Algebra.FilterBasis
/-- The topology associated to a module filter basis on a module over a topological ring.
It has the given basis as a basis of neighborhoods of zero.  -/
ModuleFilterBasis.topology : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace R] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → ModuleFilterBasis R M → TopologicalSpace M
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.integral : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E] (x : E),
  IsIntegral F x
-- Lean.Elab.DefView
Lean.Elab.HeaderProcessedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (view : Lean.Elab.DefViewElabHeaderData) (state : Lean.Elab.Term.SavedState)
  (tacStx? : Option Lean.Syntax) (tacSnap? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (bodyStx : Lean.Syntax) (bodySnap : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot))
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (toSnapshot_1 : Lean.Language.Snapshot)
  (view_1 : Lean.Elab.DefViewElabHeaderData) (state_1 : Lean.Elab.Term.SavedState) (tacStx?_1 : Option Lean.Syntax)
  (tacSnap?_1 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) (bodyStx_1 : Lean.Syntax)
  (bodySnap_1 : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot))
  (moreSnaps_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ toSnapshot := toSnapshot, view := view, state := state, tacStx? := tacStx?, tacSnap? := tacSnap?,
        bodyStx := bodyStx, bodySnap := bodySnap, moreSnaps := moreSnaps } =
      { toSnapshot := toSnapshot_1, view := view_1, state := state_1, tacStx? := tacStx?_1, tacSnap? := tacSnap?_1,
        bodyStx := bodyStx_1, bodySnap := bodySnap_1, moreSnaps := moreSnaps_1 }) =
    (toSnapshot = toSnapshot_1 ∧
      view = view_1 ∧
        state = state_1 ∧
          tacStx? = tacStx?_1 ∧
            tacSnap? = tacSnap?_1 ∧ bodyStx = bodyStx_1 ∧ bodySnap = bodySnap_1 ∧ moreSnaps = moreSnaps_1)
-- Mathlib.Order.SupClosed
finsetInf'_mem_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α} {ι : Type u_5} {t : Finset ι} (ht : t.Nonempty) {f : ι → α},
  (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ infClosure s
-- Mathlib.Topology.Inseparable
ker_nhds_eq_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, (nhds x).ker = {y | y ⤳ x}
-- Init.Data.Iterators.Consumers.Loop
Std.instForInTotalOfMonadOfIteratorLoopOfFiniteId : (α β : Type w) →
  (n : Type x → Type x') →
    [Monad n] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id n] → [Std.Iterators.Finite α Id] → ForIn n (Std.Iter.Total β) β
-- Mathlib.Analysis.LocallyConvex.Basic
/-- **Alias** of the reverse direction of `absorbs_iff_norm`. -/
Absorbs.of_norm : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
  (∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A) → Absorbs 𝕜 A B
-- Mathlib.Data.Finset.Grade
/-- **Alias** of the reverse direction of `Finset.coe_covBy_coe`. -/
CovBy.finset_coe : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → ↑s ⋖ ↑t
-- Init.Tactics
/-- `mspecialize_pure` is like `mspecialize`, but it specializes a hypothesis from the
*pure* context with hypotheses from either the pure or stateful context or pure terms.
```lean
example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
  mintro HQ
  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecializePureMacro : Lean.ParserDescr
-- Init.Data.Option.Lemmas
Option.instLawfulIdentityOrNone : ∀ {α : Type u_1}, Std.LawfulIdentity Option.or none
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minEntryD.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : (a : α) × β a),
  x.minEntryD x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => l.minEntryD fallback
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.instHasInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasInitial (CategoryTheory.WithInitial C)
-- Mathlib.Data.Finset.Powerset
Finset.ssubsets.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.ssubsets = s.powerset.erase s
-- Mathlib.RingTheory.Multiplicity
multiplicity_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α},
  Prime p → FiniteMultiplicity p (a * b) → multiplicity p (a * b) = multiplicity p a + multiplicity p b
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranAdjunction_counit : ∀ {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) (H : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F], (L.ranAdjunction H).counit = L.ranCounit
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_unsat : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [Std.IsPreorder α] (ctx : Lean.Grind.Linarith.Context α),
  Lean.Grind.Linarith.Poly.denote ctx Lean.Grind.Linarith.Poly.nil < 0 → False
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.showRules : Lean.ParserDescr
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) {Z : C}
  (h : (Φ.iterationFunctor J).obj (Order.succ j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯)) h =
    CategoryTheory.CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j))
      (CategoryTheory.CategoryStruct.comp (Φ.iterationFunctorObjSuccIso j hj).inv h)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_ne_empty : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ↑I ≠ ∅
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_mono_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊢ₛ Q') → P ∨ Q ⊢ₛ P ∨ Q'
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_eq_single_of_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} {f : ι → M},
  ∀ i ∈ s, (∀ j ∈ s, j ≠ i → f j = 0) → (s.expect fun i => f i) = (↑s.card)⁻¹ • f i
-- Mathlib.Topology.Continuous
/-- If `f x ∈ s ∈ 𝓝 (f x)` for continuous `f`, then `f y ∈ s` near `x`.

This is essentially `Filter.Tendsto.eventually_mem`, but infers in more cases when applied.  -/
ContinuousAt.eventually_mem : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X},
  ContinuousAt f x → ∀ {s : Set Y}, s ∈ nhds (f x) → ∀ᶠ (y : X) in nhds x, f y ∈ s
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.eq_def : ∀ {α : Type u} {β : Type v} (x : List ((_ : α) × β)),
  Std.Internal.List.values x =
    match x with
    | [] => []
    | ⟨fst, v⟩ :: l => v :: Std.Internal.List.values l
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_div_singleton : ∀ {α : Type u_2} [inst : Div α] {a b : α}, {a} / {b} = {a / b}
-- Mathlib.Algebra.Order.Kleene
KStar.mk : {α : Type u_5} → (α → α) → KStar α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ), CochainComplex.HomComplex.Cochain.ofHom 0 = 0
-- Batteries.Data.AssocList
Batteries.AssocList.modify.eq_def : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (f : α → β → β) (x : Batteries.AssocList α β),
  Batteries.AssocList.modify a f x =
    match x with
    | Batteries.AssocList.nil => Batteries.AssocList.nil
    | Batteries.AssocList.cons k v es =>
      match k == a with
      | true => Batteries.AssocList.cons a (f k v) es
      | false => Batteries.AssocList.cons k v (Batteries.AssocList.modify a f es)
-- Init.Data.Array.Basic
/-- Applies a function to the corresponding elements of both arrays, stopping when there are no more
elements in either array. If one array is shorter than the other, the function is passed `none` for
the missing elements.

Examples:
* `#[1, 6].zipWithAll min #[5, 2] = #[some 1, some 2]`
* `#[1, 2, 3].zipWithAll Prod.mk #[5, 6] = #[(some 1, some 5), (some 2, some 6), (some 3, none)]`
* `#[x₁, x₂].zipWithAll f #[y] = #[f (some x₁) (some y), f (some x₂) none]`
 -/
Array.zipWithAll : {α : Type u} → {β : Type u_1} → {γ : Type u_2} → (Option α → Option β → γ) → Array α → Array β → Array γ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.cpow : ∀ {f g : ℂ → ℂ} {f' g' x : ℂ},
  HasDerivAt f f' x →
    HasDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
-- Mathlib.Order.RelClasses
/-- The value from `IsWellFounded.fix` is built from the previous ones as specified.  -/
IsWellFounded.fix_eq : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {motive : α → Sort u_1}
  (ind : (x : α) → ((y : α) → r y x → motive y) → motive x) (x : α),
  IsWellFounded.fix r ind x = ind x fun y x => IsWellFounded.fix r ind y
-- Mathlib.NumberTheory.Multiplicity
/-- **Lifting the exponent lemma** for odd primes.  -/
Int.emultiplicity_pow_sub_pow : ∀ {p : ℕ},
  Nat.Prime p →
    Odd p →
      ∀ {x y : ℤ},
        ↑p ∣ x - y →
          ¬↑p ∣ x → ∀ (n : ℕ), emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} {a' : C}
  (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one : ∀ {R : Type u_1} [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (x : R), ‖x + 1‖₊ ≤ max ‖x‖₊ 1
-- Lean.DocString.Types
Lean.Doc.ListItem.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (contents : Array α), sizeOf { contents := contents } = 1 + sizeOf contents
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.mk.injEq : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (hom : u.right ⟶ v.left)
  (comm :
    autoParam
      (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
        CategoryTheory.CategoryStruct.comp hom v.hom)
      CategoryTheory.Arrow.RightHomotopy.comm._autoParam)
  (hom_1 : u.right ⟶ v.left)
  (comm_1 :
    autoParam
      (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
        CategoryTheory.CategoryStruct.comp hom_1 v.hom)
      CategoryTheory.Arrow.RightHomotopy.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Init.Data.Nat.Basic
Nat.lt_le_asymm : ∀ {a b : ℕ}, a < b → ¬b ≤ a
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_multisetProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : CommMonoid S] (t : RingCon S) (s : Multiset ι) (f : ι → S),
  ↑(Multiset.map f s).prod = (Multiset.map (fun i => ↑(f i)) s).prod
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.trans_refl : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.trans (OrderAddMonoidIso.refl β) = f
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iInf_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {x : ι → Filter α} {y : ι → Filter β},
  (∀ (i : ι), Filter.Tendsto f (x i) (y i)) → Filter.Tendsto f (iInf x) (iInf y)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  [W.RespectsIso], W.underObj.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Category.ModuleCat.Basic
CategoryTheory.Iso.toLinearEquiv_symm : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (i : X ≅ Y), i.toLinearEquiv.symm = i.symm.toLinearEquiv
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- Applying `ι S` to the preimage of `a : 𝒳` in `Fib p S` yields an object isomorphic to `a`.  -/
HasFibers.Fib.mkIsoSelf : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            {S : 𝒮} → {a : 𝒳} → (ha : p.obj a = S) → (HasFibers.ι S).obj (HasFibers.Fib.mk ha) ≅ a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k} (h : k' ∈ m.modify k f),
  (m.modify k f).get k' h = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯
-- Mathlib.Topology.UniformSpace.Defs
comp_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => s.comp s) ≤ uniformity α
-- Mathlib.Analysis.Convex.Gauge
Seminorm.gaugeSeminorm_ball : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (p : Seminorm ℝ E), gaugeSeminorm ⋯ ⋯ ⋯ = p
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.toSpecZero.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  AlgebraicGeometry.Proj.toSpecZero 𝒜 =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj 𝒜).topIso.inv
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).isoOfEq ⋯).inv
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 1)
          (AlgebraicGeometry.Spec.map
            (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers 1))))))
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : MonoidAlgebra R M}, x.coeff = 0 ↔ x = 0
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.isMax_of_succFn_le : ∀ {ι : Type u_1} [inst : LinearOrder ι] [LocallyFiniteOrder ι] (i : ι), LinearLocallyFiniteOrder.succFn i ≤ i → IsMax i
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mk.congr_simp : ∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (toProd toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A)) (e_toProd : toProd = toProd_1)
  (central : ∀ (x y : A), toProd.2 x * y = x * toProd.1 y),
  { toProd := toProd, central := central } = { toProd := toProd_1, central := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.mul_rpow : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CochainComplex.isoHomologyπ₀_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℕ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) L.isoHomologyπ₀.inv =
    CategoryTheory.CategoryStruct.comp K.isoHomologyπ₀.inv (HomologicalComplex.cyclesMap φ 0)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.Obj.inhabited : {n : ℕ} →
  (P : MvPFunctor.{u} n) → {α : TypeVec.{u} n} → [Inhabited P.A] → [(i : Fin2 n) → Inhabited (α i)] → Inhabited (↑P α)
-- Init.Data.Int.DivMod.Lemmas
Int.eq_ediv_of_mul_eq_right : ∀ {a b c : ℤ}, a ≠ 0 → a * b = c → b = c / a
-- Mathlib.MeasureTheory.Measure.Tight
MeasureTheory.IsTightMeasureSet.eq_1 : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [inst : TopologicalSpace 𝓧] (S : Set (MeasureTheory.Measure 𝓧)),
  MeasureTheory.IsTightMeasureSet S = Filter.Tendsto (⨆ μ ∈ S, ⇑μ) (Filter.cocompact 𝓧).smallSets (nhds 0)
-- Mathlib.Data.Seq.Computation
Computation.exists_of_liftRel_right : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  Computation.LiftRel R ca cb → ∀ {b : β}, b ∈ cb → ∃ a ∈ ca, R a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousSqrt.sqrt_nonneg : ∀ {R : Type u_1} {inst : LE R} {inst_1 : NonUnitalSemiring R} {inst_2 : TopologicalSpace R} [self : ContinuousSqrt R]
  (x : R × R), x.1 ≤ x.2 → 0 ≤ ContinuousSqrt.sqrt x
-- Mathlib.Analysis.Convex.Basic
convex_Iio : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β),
  Convex 𝕜 (Set.Iio r)