mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.UnionInter
Multiset.add_union_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Multiset α), s + (t ∪ u) = s + t ∪ (s + u)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalArrayExpr : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.MetaM (Array α)
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
  {ι' : Type u_5} {β' : Type u_6} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'},
  UniformCauchySeqOn F p s →
    UniformCauchySeqOn F' p' s → UniformCauchySeqOn (fun i a => (F i.1 a, F' i.2 a)) (p ×ˢ p') s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.cos (f x)) x
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_pred_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b < a → ¬IsMin b → Order.pred b < Order.pred a
-- Mathlib.Data.EReal.Basic
EReal.coe_injective : Function.Injective Real.toEReal
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.monotone_iff_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [Topology.IsLowerSet α] [Topology.IsLowerSet β] {f : α → β}, Monotone f ↔ Continuous f
-- Mathlib.Topology.NhdsWithin
Filter.Tendsto.if_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {p : α → Prop} [inst_1 : DecidablePred p]
  {a : α} {s : Set α} {l : Filter β},
  Filter.Tendsto f (nhdsWithin a (s ∩ {x | p x})) l →
    Filter.Tendsto g (nhdsWithin a (s ∩ {x | ¬p x})) l →
      Filter.Tendsto (fun x => if p x then f x else g x) (nhdsWithin a s) l
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
fn_max_mul_fn_min : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : CommSemigroup β] (f : α → β) (a b : α),
  f (max a b) * f (min a b) = f a * f b
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_hom_naturality : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} (n a a' : M) (ha' : n + a = a')
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f))
      ((F.shiftIso n a a' ha').hom.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X) ((F.shift a').map f)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.mk.injEq : ∀ {α : Type u} (next : Option α) (upperBound : α) (next_1 : Option α) (upperBound_1 : α),
  ({ next := next, upperBound := upperBound } = { next := next_1, upperBound := upperBound_1 }) =
    (next = next_1 ∧ upperBound = upperBound_1)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A singleton is a block.  -/
AddAction.IsBlock.singleton : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {a : X}, AddAction.IsBlock G {a}
-- Mathlib.Algebra.Group.Subsemigroup.Defs
isAddCommutative_iff_of_setLike : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Add M] [inst_2 : AddMemClass S M] {s : S},
  IsAddCommutative ↥s ↔ ∀ a ∈ s, ∀ b ∈ s, a + b = b + a
-- Mathlib.Data.ENat.Basic
ENat.strictMono_map_iff : ∀ {α : Type u_1} {f : ℕ → α} [inst : Preorder α], StrictMono (ENat.map f) ↔ StrictMono f
-- Init.Data.Nat.Lemmas
Nat.min_max_distrib_left : ∀ (a b c : ℕ), min a (max b c) = max (min a b) (min a c)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- To construct a morphism between left lifts, we need a 2-morphism between the lifts,
and to check that it is compatible with the units.  -/
CategoryTheory.Bicategory.LeftLift.homMk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.LeftLift f g} →
            (η : s.lift ⟶ t.lift) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerRight η f) = t.unit)
                  CategoryTheory.Bicategory.LeftLift.homMk._auto_1 →
                (s ⟶ t)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap'.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  M.mulMap' N = ↑(LinearEquiv.ofEq (M.mulMap N).range (M * N) ⋯) ∘ₗ (M.mulMap N).rangeRestrict
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasLeftHomology]
  [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) h₂.cyclesIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.cyclesIso.hom γ.φK
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C (n + 1)),
  Topology.RelCWComplex.cellFrontier (n + 1) j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.RepresentationTheory.FDRep
/-- Schur's Lemma: the dimension of the `Hom`-space between two irreducible representation is `0` if
they are not isomorphic, and `1` if they are.  -/
FDRep.finrank_hom_simple_simple : ∀ {k : Type u} {G : Type v} [inst : Field k] [inst_1 : Monoid G] [IsAlgClosed k] (V W : FDRep k G)
  [CategoryTheory.Simple V] [CategoryTheory.Simple W], Module.finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodX_ext_to_iff : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι}
  {f g : A ⟶ (K ⊞ L).X i},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.fst.f i) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.fst.f i) ∧
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biprod.snd.f i) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biprod.snd.f i)
-- Init.Data.Int.Gcd
Int.lcm_eq_left_iff_dvd : ∀ {a b : ℤ}, 0 ≤ a → (↑(a.lcm b) = a ↔ b ∣ a)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.HomIsOver.comp_over : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {S : C}
  {inst_1 : CategoryTheory.OverClass X S} {inst_2 : CategoryTheory.OverClass Y S} [self : CategoryTheory.HomIsOver f S],
  CategoryTheory.CategoryStruct.comp f (Y ↘ S) = X ↘ S
-- Mathlib.Algebra.Group.Units.Defs
/-- Copy a unit, adjusting definition equalities.  -/
Units.copy : {α : Type u} → [inst : Monoid α] → (u : αˣ) → (val : α) → val = ↑u → (inv : α) → inv = ↑u⁻¹ → αˣ
-- Mathlib.Data.DFinsupp.Defs
/-- Set `{i | f x ≠ 0}` as a `Finset`.  -/
DFinsupp.support : {ι : Type u} →
  {β : ι → Type v} →
    [DecidableEq ι] →
      [inst : (i : ι) → Zero (β i)] → [(i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Π₀ (i : ι), β i) → Finset ι
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.addTermInfo : Lean.SubExpr.Pos → Lean.Syntax → Lean.Expr → optParam Bool false → Lean.PrettyPrinter.Delaborator.DelabM Unit
-- Init.Data.Range.Polymorphic.Iterators
Std.Rci.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] →
            [Monad m] → [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] → ForIn' m (Std.Rci α) α inferInstance
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is a ring homomorphism of exponential characteristic `p` rings, such that `L`
is perfect, then the `p`-nilradical of `K` is contained in the kernel of `i`.  -/
RingHom.pNilradical_le_ker_of_perfectRing : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ) [ExpChar L p]
  [PerfectRing L p], pNilradical K p ≤ RingHom.ker i
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_nonneg : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : NumberField.InfinitePlace K),
  0 ≤ NumberField.mixedEmbedding.normAtAllPlaces x w
-- Mathlib.Control.Fold
Monoid.foldlM.mk : {m : Type u → Type u} → [inst : Monad m] → {α : Type u} → (α → m α) → Monoid.foldlM m α
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.normedSpace : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [inst_5 : Fintype ι] →
                    {𝕜' : Type u_2} →
                      [inst_6 : NormedField 𝕜'] →
                        [inst_7 : NormedSpace 𝕜' G] →
                          [SMulCommClass 𝕜 𝕜' G] → NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Data.Set.Defs
Set.ext_iff : ∀ {α : Type u} {a b : Set α}, a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_right : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → a * c ≡ b * c [MOD n]
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.support_antidiagonal_subset_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.antidiagonal hs ht a).Nonempty} ⊆ s + t
-- Mathlib.RingTheory.Ideal.Prime
Ideal.primeCompl.congr_simp : ∀ {α : Type u} [inst : Semiring α] (P P_1 : Ideal α) (e_P : P = P_1) [hp : P.IsPrime], P.primeCompl = P_1.primeCompl
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCodetector.hasDetector_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasCodetector C],
  CategoryTheory.HasDetector Cᵒᵖ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_univ : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'},
  mfderiv[Set.univ] f = mfderiv% f
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_apply : ∀ {n : ℕ}, ArithmeticFunction.cardFactors n = n.primeFactorsList.length
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsertIfNew k v).1 = t.contains k
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.prod_const : ∀ (ι : Type u) (a : Cardinal.{v}),
  (Cardinal.prod fun x => a) = Cardinal.lift.{u, v} a ^ Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- A variant of the Stone-Weierstrass theorem where `X` need not be compact:
If `A` is a subalgebra of `C(X, ℝ)` which separates points, then, for any compact set `K ⊆ X`,
every real-valued continuous function on `X` is within any `ε > 0` of some element of `A` on `K`.  -/
ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A : Subalgebra ℝ C(X, ℝ)},
  A.SeparatesPoints → ∀ (f : C(X, ℝ)) {K : Set X}, IsCompact K → ∀ {ε : ℝ}, 0 < ε → ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε
-- Mathlib.Order.Nucleus
Nucleus.sInf_apply : ∀ {X : Type u_1} [inst : CompleteLattice X] (s : Set (Nucleus X)) (x : X), (sInf s) x = ⨅ j ∈ s, j x
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_eq_cons : ∀ {α : Type u_1} {a b : α} {as bs : Multiset α},
  a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- `RingFunc.add`, but with the defeq type `Language.ring.Functions 2` instead
of `RingFunc 2`  -/
FirstOrder.Ring.addFunc : FirstOrder.Language.ring.Functions 2
-- Mathlib.Order.Category.Semilat
SemilatInfCat.instInhabited : Inhabited SemilatInfCat
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [LocallyCompactSpace M], LocallyCompactSpace Mᵃᵒᵖ
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smul_mem_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α},
  c • s ∈ MeasureTheory.ae μ ↔ s ∈ MeasureTheory.ae μ
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.sort.loop.match_1.splitter : (motive : List ℕ → List ℕ → Sort u_1) →
  (x x_1 : List ℕ) →
    ((acc : List ℕ) → motive acc []) → ((acc : List ℕ) → (x : ℕ) → (xs : List ℕ) → motive acc (x :: xs)) → motive x x_1
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {g : B →ₐ[R] C} {f : A →ₐ[R] B}, g.FinitePresentation → f.FinitePresentation → (g.comp f).FinitePresentation
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∈ t ↔ (t.get? a).isSome = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : (t.getKey? a).isSome = true}, (t.getKey? a).get h = t.getKey a ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivWithinAt.congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {x : E}, IsSymmSndFDerivWithinAt 𝕜 f s x → s =ᶠ[nhds x] t → IsSymmSndFDerivWithinAt 𝕜 f t x
-- Mathlib.LinearAlgebra.Projection
Submodule.isIdempotentElemEquiv_apply_coe : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p : Submodule R E)
  (f : { f // IsIdempotentElem f ∧ LinearMap.range f = p }), ↑(p.isIdempotentElemEquiv f) = LinearMap.codRestrict p ↑f ⋯
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.representableBy_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (Y : D) {X : C},
  (adj.representableBy Y).homEquiv = (adj.homEquiv X Y).symm
-- Mathlib.Topology.ContinuousOn
Set.Subsingleton.continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α},
  s.Subsingleton → ∀ (f : α → β), ContinuousOn f s
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.mk.injEq : ∀ (oldInlayHints : Array Lean.Elab.InlayHintInfo) (oldFinishedSnaps : ℕ) (lastEditTimestamp? : Option ℕ)
  (isFirstRequestAfterEdit : Bool) (oldInlayHints_1 : Array Lean.Elab.InlayHintInfo) (oldFinishedSnaps_1 : ℕ)
  (lastEditTimestamp?_1 : Option ℕ) (isFirstRequestAfterEdit_1 : Bool),
  ({ oldInlayHints := oldInlayHints, oldFinishedSnaps := oldFinishedSnaps, lastEditTimestamp? := lastEditTimestamp?,
        isFirstRequestAfterEdit := isFirstRequestAfterEdit } =
      { oldInlayHints := oldInlayHints_1, oldFinishedSnaps := oldFinishedSnaps_1,
        lastEditTimestamp? := lastEditTimestamp?_1, isFirstRequestAfterEdit := isFirstRequestAfterEdit_1 }) =
    (oldInlayHints = oldInlayHints_1 ∧
      oldFinishedSnaps = oldFinishedSnaps_1 ∧
        lastEditTimestamp? = lastEditTimestamp?_1 ∧ isFirstRequestAfterEdit = isFirstRequestAfterEdit_1)
-- Std.Data.Iterators.Lemmas.Producers.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it : Std.IterM m α)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.subset : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s t : Set ι} {f : ι → α},
  t.PairwiseDisjoint f → s ⊆ t → s.PairwiseDisjoint f
-- Mathlib.Data.List.Cycle
/-- We define a representation of concrete cycles, available when viewing them in a goal state or
via `#eval`, when over representable types. For example, the cycle `(2 1 4 3)` will be shown
as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
is different.
 -/
Cycle.instRepr : {α : Type u_1} → [Repr α] → Repr (Cycle α)
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.map_f : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {k : WithTop ℕ∞}
  {E : Type u_4} {H : Type u_5} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
  [inst_4 : FiniteDimensional ℝ E] [inst_5 : TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  (s : SingularManifold X k I) {φ : X → Y} (hφ : Continuous φ), (s.map hφ).f = φ ∘ s.f
-- Mathlib.Algebra.Group.Fin.Basic
/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too.  -/
Fin.instIsCancelAdd : ∀ (n : ℕ), IsCancelAdd (Fin n)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.lift_map : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] {P : C} (k : (j : J) → P ⟶ f j) (p : (j : J) → f j ⟶ g j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift k) (CategoryTheory.Limits.biproduct.map p) =
    CategoryTheory.Limits.biproduct.lift fun j => CategoryTheory.CategoryStruct.comp (k j) (p j)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a_one_pow : ∀ {n : ℕ} (k : ℕ), QuaternionGroup.a 1 ^ k = QuaternionGroup.a ↑k
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- If `g` is continuous multilinear and `f` is a collection of continuous linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a continuous multilinear map, that we call
`g.compContinuousLinearMap f`.  -/
ContinuousMultilinearMap.compContinuousLinearMap : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₁' : ι → Type w₁'} →
        {M₄ : Type w₄} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : (i : ι) → AddCommMonoid (M₁' i)] →
                [inst_3 : AddCommMonoid M₄] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : (i : ι) → Module R (M₁' i)] →
                      [inst_6 : Module R M₄] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : (i : ι) → TopologicalSpace (M₁' i)] →
                            [inst_9 : TopologicalSpace M₄] →
                              ContinuousMultilinearMap R M₁' M₄ →
                                ((i : ι) → M₁ i →L[R] M₁' i) → ContinuousMultilinearMap R M₁ M₄
-- Init.Data.Vector.Lemmas
Vector.getElem?_empty : ∀ {α : Type u_1} {i : ℕ}, #v[][i]? = none
-- Init.Data.Array.Lex.Lemmas
Array.not_le_iff_gt : ∀ {α : Type u_1} [inst : LT α] {xs ys : Array α}, ¬xs ≤ ys ↔ ys < xs
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.toPerfPair.congr_simp : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p p_1 : M →ₗ[R] N →ₗ[R] R) (e_p : p = p_1) [inst_5 : p.IsPerfPair],
  p.toPerfPair = p_1.toPerfPair
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.containsKey.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.Internal.List.containsKey a l)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_subsingleton : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : CommMonoid M] [Subsingleton ι] (f : ι → M) (a : ι),
  ∏ x, f x = f a
-- Mathlib.Topology.Order.OrderClosed
CovBy.nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b ⋖ a → nhdsWithin b (Set.Ioi b) = ⊥
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X Y : C}
  (f : Y ⟶ X) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).hom.app X_1).left =
    CategoryTheory.Over.Hom.left
      (((((((CategoryTheory.Over.map f).leftUnitor.symm.homCongr
                          ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                                (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))).rightUnitor.symm).trans
                      (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                          ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                            (CategoryTheory.Over.forget (CategoryTheory.Over.mk f)))
                          (CategoryTheory.Over.map f) (CategoryTheory.Functor.id (CategoryTheory.Over X))).symm).trans
                  (CategoryTheory.mateEquiv
                    ((CategoryTheory.Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp
                      (CategoryTheory.forgetAdjToOver (CategoryTheory.Over.mk f)))
                    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f))).trans
              (CategoryTheory.TwoSquare.equivNatTrans
                ((CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp
                  (CategoryTheory.Over.mk f).iteratedSliceForward)
                (CategoryTheory.Functor.id (CategoryTheory.Over X)) (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                (CategoryTheory.ChosenPullbacksAlong.pullback f)))
            (CategoryTheory.eqToHom ⋯)).app
        X_1)