mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is line differentiable at `x₀` and `C`-lipschitz
then its line derivative at `x₀` in the direction `v` has norm bounded by `C * ‖v‖`.  -/
HasLineDerivAt.le_of_lipschitz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {f' : F} {x₀ : E}, HasLineDerivAt 𝕜 f f' x₀ v → ∀ {C : NNReal}, LipschitzWith C f → ‖f'‖ ≤ ↑C * ‖v‖
-- Mathlib.Algebra.Module.LinearMap.End
Module.toModuleEnd_apply : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] (s : S),
  (Module.toModuleEnd R M) s = DistribSMul.toLinearMap R M s
-- Mathlib.Algebra.Star.StarAlgHom
/-- By definition, a ⋆-algebra equivalence commutes with the action of scalars.  -/
StarAlgEquiv.map_smul' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (self : A ≃⋆ₐ[R] B) (r : R) (a : A),
  self.toFun (r • a) = r • self.toFun a
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) (ij : n × m), A.vec ij = A ij.2 ij.1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.isWrap : Lean.Expr → Option Lean.Expr
-- Mathlib.Probability.Martingale.Convergence
MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_of_splits_copy : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.copy.Splits t₁ t₂ → p.Splits t₁ t₂
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.closedPoint.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : IsLocalRing R],
  IsLocalRing.closedPoint R = { asIdeal := IsLocalRing.maximalIdeal R, isPrime := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atTop_eq_generate_of_forall_exists_le : ∀ {α : Type u_3} [inst : Preorder α] {s : Set α},
  (∀ (x : α), ∃ y ∈ s, x ≤ y) → Filter.atTop = Filter.generate (Set.Ici '' s)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_deleteEdges_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)),
  (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)
-- Mathlib.Analysis.Distribution.TestFunction
/-- Notation for the space of bundled `n`-times continuously differentiable maps
with compact support.  -/
Distributions.«term𝓓^{_}(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.subsingleton : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul A B a0 b0 → Subsingleton { ab // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 }
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernel.π_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.Limits.cokernel.π f.op).unop =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelOpUnop f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle.eq_1 : Polynomial.toAddCircle =
  Polynomial.aeval { toFun := fun c => ↑c.toCircle, continuous_toFun := Polynomial.toAddCircle._proof_1 }
-- Mathlib.Tactic.Linter.Whitespace
/-- The starting position of the mismatch, as a `String.pos`.  -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.srcStartPos : Mathlib.Linter.FormatError✝ → String.Pos.Raw
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
-- Mathlib.Analysis.Convex.Integral
/-- If `f : α → E` is an integrable function, then either it is a.e. equal to the constant
`⨍ x, f x ∂μ` or there exists a measurable set such that `μ t ≠ 0`, `μ tᶜ ≠ 0`, and the average
values of `f` over `t` and `tᶜ` are different.  -/
ae_eq_const_or_exists_average_ne_compl : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable f μ →
    f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨
      ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
-- Lean.DocString.Types
Lean.Doc.ListItem.mk : {α : Type u} → Array α → Lean.Doc.ListItem α
-- Init.Data.List.Count
List.countP_eq_length_filter' : ∀ {α : Type u_1} {p : α → Bool}, List.countP p = List.length ∘ List.filter p
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_whiskerLeft : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (η : G ⟶ H),
  CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (F.whiskerLeft η) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F G).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).whiskerLeft
          (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) η))
        (CategoryTheory.Join.mapCompRight A F H).inv)
-- Mathlib.Data.Finsupp.Single
Finsupp.support_update_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) [inst_1 : DecidableEq α],
  (f.update a 0).support = f.support.erase a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 0 < a → a < 1 → m < n → a ^ n < a ^ m
-- Mathlib.RingTheory.Spectrum.Prime.Homeomorph
/-- Purely inseparable field extensions are universal homeomorphisms.  -/
PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable : ∀ (k : Type u_1) (K : Type u_2) (R : Type u_3) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : CommRing R] [inst_4 : Algebra k R] [IsPurelyInseparable k K],
  IsHomeomorph (PrimeSpectrum.comap (algebraMap R (TensorProduct k R K)))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.mk : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Zipper α β → α → Std.DTreeMap.Internal.RxoIterator α β
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_hom_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] {F_1 : D → D → Type uF}
  {carrier : D → Type w} {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory D F_1] (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.inv f)))
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.id : Lean.Meta.Grind.Arith.CommRing.Semiring → ℕ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.lift_eta : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop),
  CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
      ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteGrp.ProfiniteCompletion.lift f)) =
    f
-- Lean.MetavarContext
Lean.LocalInstances : Type
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.Cocone.isColimit_iff_isIso_colimMap_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [inst_2 : CategoryTheory.IsConnected J] {F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasColimit F]
  (c : CategoryTheory.Limits.Cocone F),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.colimMap c.ι)
-- Mathlib.Topology.Order.SuccPred
PredOrder.nhds_eq_pure : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α}, nhds a = pure a ↔ ¬Order.IsPredLimit a
-- Mathlib.Algebra.Ring.Commute
mul_self_eq_one_iff : ∀ {R : Type u} [inst : NonAssocRing R] [NoZeroDivisors R] {a : R}, a * a = 1 ↔ a = 1 ∨ a = -1
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Config.mk : ℕ → Option String → (Lean.Name → Lean.MetaM Bool) → Option String → Lean.LibrarySuggestions.Config
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.rfl : ∀ {α : Type u} {β : Type v} {l : Filter α} {f : α → β}, f =ᶠ[l] f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.file.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.file = 1
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- General result on bounding q-expansion coefficients using a bound on the norm of the function.
This will get used twice over, once for cusp forms (with `e = k / 2`) and once for modular forms
(with `e = k`).  -/
qExpansion_coeff_isBigO_of_norm_isBigO : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
  [ModularFormClass F Γ k] (f : F) (e : ℝ),
  (⇑f =O[Filter.comap UpperHalfPlane.im (nhds 0)] fun τ => τ.im ^ (-e)) →
    (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n => ↑n ^ e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMinEntryD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.minEntryD t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.minEntryD t₂ fallback
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.ι_image_homOfLE_eq_ι_image_inf : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : (↑V).Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W) =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W ⊓ U
-- Mathlib.Algebra.Vertex.VertexOperator
HVertexOperator.coeff.eq_1 : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W],
  HVertexOperator.coeff =
    { toFun := fun A n => { toFun := fun v => ((HahnModule.of R).symm (A v)).coeff n, map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J]
  [inst_12 : K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₁.π c₂ c (i₁, i₂) = j) {Z : D}
  (h : (K₂.mapBifunctor K₁ F.flip c).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj)
      (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorFlipIso K₂ F c).inv.f j) h) =
    CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j ⋯) h
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop : (n : ℕ) → ((i : ℕ) → i < n → Bool) → (i : ℕ) → i ≤ n → Bool
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasColimitsOfShape : ∀ (J : Type v) [inst : CategoryTheory.Category.{v_1, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasColimitsOfShape J TopCat
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_vadd_eq_of_nonempty : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄, ((g +ᵥ B) ∩ B).Nonempty → g +ᵥ B = B
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_apply_ofCard : ∀ {R : Type u_1} {M : Type u_2} {n : ℕ} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] (b : Module.Basis I R M) {s : Finset I} (s_card : s.card = n),
  b.ExteriorAlgebra s = ExteriorAlgebra.ιMulti_family R n (⇑b) (Set.powersetCard.ofCard s_card)
-- Mathlib.Order.Disjoint
Complementeds.instDistribLattice : {α : Type u_1} → [inst : DistribLattice α] → [inst_1 : BoundedOrder α] → DistribLattice (Complementeds α)
-- Init.CbvSimproc
Lean.Parser.cbvSimprocEval : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_erase : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, (s.erase a)ᶜ = insert a sᶜ
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.eq_affineLocally : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  P = AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If an affine combination of affinely independent points lies in the affine span of a subset
of those points, all weights outside that subset are zero.  -/
AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {fs : Finset ι} {w : ι → k},
      ∑ i ∈ fs, w i = 1 →
        ∀ {s : Set ι}, (Finset.affineCombination k fs p) w ∈ affineSpan k (p '' s) → ∀ {i : ι}, i ∈ fs → i ∉ s → w i = 0
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.mk.injEq : ∀ (toInteractiveGoalCore : Lean.Widget.InteractiveGoalCore) (range : Lean.Lsp.Range)
  (term : Lean.Server.WithRpcRef Lean.Elab.TermInfo) (toInteractiveGoalCore_1 : Lean.Widget.InteractiveGoalCore)
  (range_1 : Lean.Lsp.Range) (term_1 : Lean.Server.WithRpcRef Lean.Elab.TermInfo),
  ({ toInteractiveGoalCore := toInteractiveGoalCore, range := range, term := term } =
      { toInteractiveGoalCore := toInteractiveGoalCore_1, range := range_1, term := term_1 }) =
    (toInteractiveGoalCore = toInteractiveGoalCore_1 ∧ range = range_1 ∧ term = term_1)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀' : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ),
  CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))) →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀'._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀'._auto_3),
      CategoryTheory.IsIso (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Topology.Algebra.AsymptoticCone
isClosed_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P},
  IsClosed (asymptoticCone k s)
-- Batteries.Data.String.Matcher
String.Matcher.mk.inj : ∀ {toMatcher : Array.Matcher Char} {pattern : Substring.Raw} {toMatcher_1 : Array.Matcher Char}
  {pattern_1 : Substring.Raw},
  { toMatcher := toMatcher, pattern := pattern } = { toMatcher := toMatcher_1, pattern := pattern_1 } →
    toMatcher = toMatcher_1 ∧ pattern = pattern_1
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.eq_add_of_ne_all : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G] {x y z : G},
  x ≠ 0 → y ≠ 0 → x ≠ y → z ≠ 0 → z ≠ x → z ≠ y → z = x + y
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_empty : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : DecidableLE α] [inst_2 : OrderTop α] (a : α), ∅.truncatedSup a = ⊤
-- Mathlib.Topology.EMetricSpace.Basic
/-- If a map between pseudoemetric spaces is a uniform inducing map then the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`.  -/
EMetric.controlled_of_isUniformInducing : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  IsUniformInducing f →
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.ext : ∀ {R : Type u_1} {inst : CommRing R} {x y : RingPreordering R}, (↑x).carrier = (↑y).carrier → x = y
-- Mathlib.Data.Set.Card
Set.encard_union_add_encard_inter : ∀ {α : Type u_1} (s t : Set α), (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
-- Mathlib.Data.QPF.Univariate.Basic
QPF.liftr_iff : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (r : α → α → Prop) (x y : F α),
  Functor.Liftr r x y ↔ ∃ a f₀ f₁, x = QPF.abs ⟨a, f₀⟩ ∧ y = QPF.abs ⟨a, f₁⟩ ∧ ∀ (i : (QPF.P F).B a), r (f₀ i) (f₁ i)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.zero_le_degree_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 ≤ p.degree ↔ p ≠ 0
-- Lean.Parser.Command
/-- Skip input until the next character that satisfies the predicate, then skip whitespace  -/
_private.Lean.Parser.Command.0.Lean.Parser.Command.skipUntil : (Char → Bool) → Lean.Parser.Parser
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.map_apply : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type v} (f : β → γ) (g : α →𝒄 Part β) (x : α),
  (OmegaCompletePartialOrder.ContinuousHom.map f g) x = Part.map f (g x)
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.traceDual_top : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [inst_15 : Decidable (IsField A)],
  Submodule.traceDual A K ⊤ = if IsField A then ⊤ else ⊥
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.instPartialOrder : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → PartialOrder (L.PartialEquiv M N)
-- Init.Data.Option.Lemmas
Option.any_join : ∀ {α : Type u_1} {p : α → Bool} {x : Option (Option α)}, Option.any p x.join = Option.any (Option.any p) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.getKey! a = (m.getKey? a).get!
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_left_inverse : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] {B₁ : LinearMap.BilinMap R M N},
  (∀ (x y : M), (B₁ x) y = (B₁ y) x) → (QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a bifunctor `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂`, and morphisms `f₁ : X₁ ⟶ Y₁` in `C₁`
and `f₃ : X₃ ⟶ Y₃` in `C₃`, this structure contains the data of
a pullback of `(G.obj (op X₁)).obj X₃`
and `(G.obj (op Y₁)).obj Y₃` over `(G.obj (op X₁)).obj Y₃`.  -/
CategoryTheory.Functor.PullbackObjObj : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂) →
              {X₁ Y₁ : C₁} → (X₁ ⟶ Y₁) → {X₃ Y₃ : C₃} → (X₃ ⟶ Y₃) → Type (max u₂ v₂)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.mk.sizeOf_spec : ∀ (subgoals : List Lean.Expr) (instVal instTypeBody : Lean.Expr),
  sizeOf { subgoals := subgoals, instVal := instVal, instTypeBody := instTypeBody } =
    1 + sizeOf subgoals + sizeOf instVal + sizeOf instTypeBody
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add_supp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedAddCommMonoidWithTop Γ₀] [inst_1 : CommRing R]
  (v : AddValuation R Γ₀) (a : R) {s : R}, s ∈ v.supp → v (a + s) = v a
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.matchType : Lean.Elab.Term.ElabMatchTypeAndDiscrsResult → Lean.Expr
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.cpolynomialAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → CPolynomialAt 𝕜 f x