mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_symmDiff : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s t : Set α) (f : α → M),
  (symmDiff s t).mulIndicator f = (s \ t).mulIndicator f * (t \ s).mulIndicator f
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The canonical `RightHomologyData` of a short complex `S` in an abelian category, for
which the `H` field is `Abelian.image (kernel.ι S.g ≫ cokernel.π S.f)`.  -/
CategoryTheory.ShortComplex.RightHomologyData.ofAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex C) → S.RightHomologyData
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → n < Function.minimalPeriod f x → n = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, s.Nonempty → t.Nonempty → (s * t).Nonempty
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.extension_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [T0Space β],
  UniformContinuous f → ∀ (a : α), UniformSpace.Completion.extension f ↑a = f a
-- Batteries.Data.Array.Match
Array.PrefixTable.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (toArray : Array (α × ℕ))
  (valid : ∀ {i : ℕ} (h : i < toArray.size), toArray[i].2 ≤ i),
  sizeOf { toArray := toArray, valid := valid } = 1 + sizeOf toArray
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` preserves epimorphisms (G5).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  F.PreservesEpimorphisms
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), f.comp (OrderAddMonoidHom.id α) = f
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotEquivQuotSupₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotEquivQuotSup I J)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- A multivariate power series can be substituted if and only if
it can be evaluated when the topology on the coefficients ring is the discrete topology.  -/
MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S}
  [inst_1 : TopologicalSpace S] [DiscreteTopology S], MvPowerSeries.HasSubst a ↔ MvPowerSeries.HasEval a
-- Mathlib.Order.Filter.SmallSets
/-- **Alias** of the forward direction of `Filter.eventually_smallSets_forall`. -/
Filter.Eventually.of_smallSets : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop}, (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) → ∀ᶠ (x : α) in l, p x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Being `C^n` in a set only depends on the germ of the set. Version where one only requires
the two sets to coincide locally in the complement of a point `y`.  -/
contMDiffWithinAt_congr_set' : ∀ {𝕜 : 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'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞} (y : M),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_eq_top : ∀ {α : Type u} [inst : CommSemiring α] {x : α}, Ideal.span {x} = ⊤ ↔ IsUnit x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for bitwise xor of `BitVec`s.  -/
BitVec.reduceXOr : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a`, `b`, and `c`, the derivative `f'` is nonpositive on
`Ioo a b` and nonnegative on `Ioo b c`. Then `f` attains its minimum on `Icc a c` at `b`.  -/
isMinOn_Icc_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      ContinuousAt f c →
        DifferentiableOn ℝ f (Set.Ioo a b) →
          DifferentiableOn ℝ f (Set.Ioo b c) →
            (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Icc a c) b
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.requestCancellationPromise : Lean.Server.RequestCancellationToken → IO.Promise Unit
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.comp_assoc : ∀ {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : CategoryTheory.ReflQuiver U]
  [inst_1 : CategoryTheory.ReflQuiver V] [inst_2 : CategoryTheory.ReflQuiver W] [inst_3 : CategoryTheory.ReflQuiver Z]
  (F : U ⥤rq V) (G : V ⥤rq W) (H : W ⥤rq Z), F ⋙rq G ⋙rq H = F ⋙rq (G ⋙rq H)
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Icc_of_monotoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → MonotoneOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (f a) (f b)
-- Mathlib.SetTheory.Ordinal.Basic
/-- The underlying type of the order.  -/
WellOrder.α : WellOrder → Type u
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integral_eq_of_tendsto_of_nonneg_ae : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [l.NeBot]
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ℝ} (I : ℝ),
      0 ≤ᵐ[μ] f →
        (∀ (n : ι), MeasureTheory.IntegrableOn f (φ n) μ) →
          Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (nhds I) → ∫ (x : α), f x ∂μ = I
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppAddEquivProdFinsupp_apply : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M),
  Finsupp.sumFinsuppAddEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯)
-- Mathlib.RingTheory.Adjoin.FG
/-- The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring.  -/
AlgHom.isNoetherianRing_range : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) [IsNoetherianRing A], IsNoetherianRing ↥f.range
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.prop_ι_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory),
  P (P.ι.obj X)
-- Mathlib.Data.Nat.Init
Nat.le_div_two_iff_mul_two_le : ∀ {n m : ℕ}, m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n
-- Init.Data.String.Iterator
String.Iterator.hasNext : String.Legacy.Iterator → Bool
-- Mathlib.Probability.Distributions.Pareto
/-- The Lebesgue integral of the Pareto pdf over reals `≤ t` equals `0`.  -/
ProbabilityTheory.lintegral_paretoPDF_of_le : ∀ {t r x : ℝ}, x ≤ t → ∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.paretoPDF t r y = 0
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_union_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousMul α] {s t : Set β},
  Disjoint s t →
    Multipliable (f ∘ Subtype.val) →
      Multipliable (f ∘ Subtype.val) → ∏' (x : ↑(s ∪ t)), f ↑x = (∏' (x : ↑s), f ↑x) * ∏' (x : ↑t), f ↑x
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Post-composition of a `Bundle.Trivialization` and a `Homeomorph`.  -/
Bundle.Trivialization.homeomorphComp : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              Bundle.Trivialization F proj →
                {B' : Type u_5} → [inst_3 : TopologicalSpace B'] → (h : B ≃ₜ B') → Bundle.Trivialization F (⇑h ∘ proj)
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.instIsLocallyArtinianToScheme : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyArtinian X] {U : X.Opens},
  AlgebraicGeometry.IsLocallyArtinian ↑U
-- Init.Data.String.Lemmas.Search
String.back_eq : ∀ {s : String}, s.back = s.back?.getD default
-- Init.Data.SInt.Lemmas
Int8.ofInt_sub : ∀ (a b : ℤ), Int8.ofInt (a - b) = Int8.ofInt a - Int8.ofInt b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.ncard_inter : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∈ C → (s ∩ c.supp).ncard = 1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀_mul : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (r s : (i : ι) → G i),
  DirectLimit.map₀ f (r * s) = DirectLimit.map₀ f r * DirectLimit.map₀ f s
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Pi.repr.eq_1 : ∀ {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄
  (x : MvQPF.Pi F α),
  MvQPF.Pi.repr F x = ⟨fun a => (MvQPF.repr (x a)).fst, fun _i a => (MvQPF.repr (x a.fst)).snd _i a.snd⟩
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureStep_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult.go.match_1.eq_1 : ∀ (motive : Option Lean.SyntaxNodeKind → Sort u_1) (kind : Lean.SyntaxNodeKind)
  (h_1 : (kind : Lean.SyntaxNodeKind) → motive (some kind)) (h_2 : (x : Option Lean.SyntaxNodeKind) → motive x),
  (match some kind with
    | some kind => h_1 kind
    | x => h_2 x) =
    h_1 kind
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_subset_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} {s : Affine.Simplex k P n},
  s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))
-- Mathlib.RingTheory.Ideal.Basis
/-- A basis on `S` gives a basis on `Ideal.span {x}`, by multiplying everything by `x`.  -/
Ideal.basisSpanSingleton : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommRing S] →
          [IsDomain S] →
            [inst_3 : Algebra R S] → Module.Basis ι R S → {x : S} → x ≠ 0 → Module.Basis ι R ↥(Ideal.span {x})
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexEquivIcc_apply_coe : ∀ (𝕜 : Type u_1) [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜] (f : ↑(stdSimplex 𝕜 (Fin 2))),
  ↑((stdSimplexEquivIcc 𝕜) f) = ↑f 1
-- Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.evalDSimpTrace : Lean.Elab.Tactic.Tactic
-- Init.Data.String.Basic
/-- Given a position in `s` that is between `p₀` and `p₁`, obtain the corresponding position in
`s.slice p₀ p₁ h`.  -/
String.Pos.slice : {s : String} → (pos p₀ p₁ : s.Pos) → (h₁ : p₀ ≤ pos) → (h₂ : pos ≤ p₁) → (s.slice p₀ p₁ ⋯).Pos
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.All.lowerBound? : ∀ {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.All p t → RBTree.RBNode.lowerBound? cut t = some x → p x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b h) (t.truncLTι b) = t.truncLTι a
-- Mathlib.RingTheory.Localization.Basic
/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
 -/
IsLocalization.algebraMap_eq_map_map_submonoid : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ], algebraMap Rₘ Sₘ = IsLocalization.map Sₘ (algebraMap R S) ⋯
-- Std.Time.Internal.UnitVal
/-- Converts an `Offset` to another unit type.
 -/
Std.Time.Internal.UnitVal.convert : {a b : ℚ} → Std.Time.Internal.UnitVal a → Std.Time.Internal.UnitVal b
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The diagram restricted to `Over i'`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.D' : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
                    A.𝒰D.I₀ → CategoryTheory.Functor (CategoryTheory.Over A.i') AlgebraicGeometry.Scheme
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map sending `x : H → A` to `(g : G) ↦ φ (x (f g))`.  -/
groupCohomology.cochainsMap₁ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k H} →
          {B : Rep.{u_1, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (ModuleCat.of k (H → ↑A) ⟶ ModuleCat.of k (G → ↑B))
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- A submonoid `S` of an additive monoid `R` is (left) Ore if common summands on the right can be
turned into common summands on the left, and if each pair of `r : R` and `s : S` admits an Ore
minuend `v : R` and an Ore subtrahend `u : S` such that `u + r = v + s`.  -/
AddOreLocalization.AddOreSet : {R : Type u_1} → [inst : AddMonoid R] → AddSubmonoid R → Type u_1
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.mk : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} [topology : TopologicalSpace E], topology = p.moduleFilterBasis.topology → WithSeminorms p
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.mk.injEq : ∀ (newText : String) (insert replace : Lean.Lsp.Range) (newText_1 : String) (insert_1 replace_1 : Lean.Lsp.Range),
  ({ newText := newText, insert := insert, replace := replace } =
      { newText := newText_1, insert := insert_1, replace := replace_1 }) =
    (newText = newText_1 ∧ insert = insert_1 ∧ replace = replace_1)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_eq_zero_of_ediam_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = ⊤ → G.diam = 0
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_think : ∀ {α : Type u} (s : Stream'.WSeq α), s.think.head = s.head.think
-- Init.Data.Array.Lemmas
Array.all_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (Array.replicate n a).all f = if n = 0 then true else f a
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_const : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] [inst_5 : MeasureTheory.IsFiniteMeasure μ] (c : Mᵈᵃᵃ) (a : E),
  c +ᵥ (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.eq →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.lt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        r.toListModel
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraMap_apply' : ∀ {R : Type u_1} (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (p : Polynomial R), (algebraMap (Polynomial R) (PowerSeries A)) p = (PowerSeries.map (algebraMap R A)) ↑p
-- Init.Data.Array.Extract
Array.takeWhile_replicate_eq_filter : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  Array.takeWhile p (Array.replicate n a) = Array.filter p (Array.replicate n a)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_of_not_dvd : ∀ {p n : ℕ}, ¬p ∣ n → p.maxPowDvdDiv n = (0, n)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.inv.eq_1 : ∀ (G : Type v) [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G], IsometryEquiv.inv G = { toEquiv := Equiv.inv G, isometry_toFun := ⋯ }
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.inhabited : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → Inhabited (MulChar R R')
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of `s` is the smallest normal subgroup containing `s`.  -/
Subgroup.normalClosure_le_normal : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {N : Subgroup G} [N.Normal], s ⊆ ↑N → Subgroup.normalClosure s ≤ N
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.step_done : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Zipper.done.step = Std.IterStep.done
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.Data.Multiset.Defs
/-- `s ≤ t` means that `s` is a sublist of `t` (up to permutation).
Equivalently, `s ≤ t` means that `count a s ≤ count a t` for all `a`.  -/
Multiset.Le : {α : Type u_1} → Multiset α → Multiset α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.isBipartite_bipartiteDoubleCover : ∀ {V : Type u_1} {G : SimpleGraph V}, G.bipartiteDoubleCover.IsBipartite
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConcaveOn s φ f → UniformConvexOn s φ (-f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β k → β k} {hc : k ∈ t.modify k f},
  (t.modify k f).getKey k hc = k
-- Lean.Parser.Command
/-- `openDecl` is the body of an `open` declaration (see `open`)  -/
Lean.Parser.Command.openDecl : Lean.Parser.Parser
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
TopCat.presheafToTypes_obj : ∀ (X : TopCat) {T : ↑X → Type u_1} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ},
  (X.presheafToTypes T).obj U = ((x : ↥(Opposite.unop U)) → T ↑x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_union_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.enorm_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖((InnerProductSpace.rankOne 𝕜) x) y‖ₑ = ‖x‖ₑ * ‖y‖ₑ
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) {m₁ : J}
  (φ : (x : Subtype D.P) → ↑x ⟶ m₁) (a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄ D φ).P a = (D.P a ∨ m₁ = a)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.sub.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.sub q₁ q₂ =
    q₁.liftOn₂ q₂
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (c, d) => Lean.Grind.Ring.OfSemiring.Q.mk (a + d, c + b))
      ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_comp_ofList : ∀ {α : Type u_1}, ⇑FreeAddMonoid.toList ∘ ⇑FreeAddMonoid.ofList = id
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A class that carries the non-Prop data required to define a right action of
a monoidal category `C` on a category `D`, to set up notations.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategoryStruct C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Order.RelSeries
RelSeries.toList_singleton : ∀ {α : Type u_1} {r : SetRel α α} (x : α), (RelSeries.singleton r x).toList = [x]
-- Mathlib.LinearAlgebra.Projection
Submodule.coe_projectionOnto_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), ↑((p.projectionOnto q hpq) x) = (p.projection q hpq) x
-- Init.Data.Int.DivMod.Lemmas
Int.emod_add_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (x % ↑n + y).bmod n = (x + y).bmod n