mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given two distinct points on a sphere, the inner product of the chord with
the radius vector at one endpoint is negative.  -/
EuclideanGeometry.inner_vsub_center_vsub_pos : ∀ {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} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → 0 < inner ℝ (p₂ -ᵥ p₁) (s.center -ᵥ p₁)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_add : ∀ {R : Type u} [inst : Semiring R] {a b : AddMonoidAlgebra R ℕ},
  { toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
-- Mathlib.Data.List.Induction
List.recNeNil_singleton : ∀ {α : Type u_1} {motive : (l : List α) → l ≠ [] → Sort u_2} (x : α) (singleton : (x : α) → motive [x] ⋯)
  (cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯),
  List.recNeNil singleton cons [x] ⋯ = singleton x
-- Init.Data.SInt.Lemmas
ISize.toInt_minValue_lt_zero : ISize.minValue.toInt < 0
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.card_cycleType_eq_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.cycleType.card = 0 ↔ σ = 1
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}
  {s : Set (E × F)}, DifferentiableWithinAt 𝕜 Prod.fst s p
-- Mathlib.Topology.MetricSpace.Bounded
/-- Characterization of the boundedness of the range of a function  -/
Metric.isBounded_range_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α},
  Bornology.IsBounded (Set.range f) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instContinuousFourier : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V]
  [inst_6 : BorelSpace V], ContinuousFourier (SchwartzMap V E) (SchwartzMap V E)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_liftInner : ∀ {α : Type u_1} {γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : MonadLiftT m n] [LawfulMonadLiftT m n] {x : Std.Iterators.HetT m α}
  {f : (a : α) → (Std.Iterators.HetT.liftInner n x).Property a → m γ},
  ((Std.Iterators.HetT.liftInner n x).prun fun a ha => liftM (f a ha)) = liftM (x.prun f)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h : ¬r.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 : l.size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2)
  (size : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_3 : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size)
  (h_4 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size),
  l = Std.DTreeMap.Internal.Impl.inner size lk lv ll lr →
    h ≍ h_3 →
      h_1 ≍ h_4 →
        (match l, h, h_1 with
          | Std.DTreeMap.Internal.Impl.leaf, h, h_5 => h_1_1 h h_5
          | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_5 => h_2 size lk lv ll lr h h_5) ≍
          h_2 size lk lv ll lr h_3 h_4
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The derivative of the L-series of `f` agrees with the negative of the L-series of
`log * f` on the right half-plane of absolute convergence.  -/
LSeries_deriv_eqOn : ∀ {f : ℕ → ℂ}, Set.EqOn (deriv (LSeries f)) (-LSeries (LSeries.logMul f)) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
-- Init.Data.Int.Linear
Int.Internal.Linear.mul_eq_zero_right : ∀ (a b : ℤ), b = 0 → a * b = 0
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `takeD`.  -/
List.takeDTR : {α : Type u_1} → ℕ → List α → α → List α
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_neg_one : ∀ (x : ENNReal), x ^ (-1) = x⁻¹
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.evaluationUncurried_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x y : C × CategoryTheory.Functor C D} (f : x ⟶ y),
  (CategoryTheory.evaluationUncurried C D).map f = CategoryTheory.CategoryStruct.comp (x.2.map f.1) (f.2.app y.1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).functor.obj F = F.functor
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.mk = (AddMonoid.coprodCon M N).mk'
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderEmbedding.inter_preimage_setOfPred_maximal_eq_of_subset`. -/
OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β} {t : Set β},
  t ⊆ ⇑f '' s → (x ∈ s ∩ ⇑f ⁻¹' {y | Maximal (fun x => x ∈ t) y} ↔ Maximal (fun x => x ∈ s ∩ ⇑f ⁻¹' t) x)
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compChangeOfVariables.eq_1 : ∀ (m M N : ℕ) (i : (n : ℕ) × (Fin n → ℕ)) (hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N),
  FormalMultilinearSeries.compChangeOfVariables m M N i hi =
    Sigma.casesOn (motive := fun x => x ∈ FormalMultilinearSeries.compPartialSumSource m M N → (n : ℕ) × Composition n)
      i (fun n f hi => ⟨∑ j, f j, { blocks := List.ofFn fun a => f a, blocks_pos := ⋯, blocks_sum := ⋯ }⟩) hi
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findRev?_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.findRev? p).isSome = true ↔ ∃ i, p i = true
-- Lean.Meta.AppBuilder
/-- Given `h : a ≍ b` where `a` and `b` have the same type, returns a proof of `a = b`.  -/
Lean.Meta.mkEqOfHEq : Lean.Expr → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.Logic.Pairwise
Set.Pairwise.on_injective : ∀ {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} {s : Set α},
  s.Pairwise r → Function.Injective f → (∀ (x : ι), f x ∈ s) → Pairwise (Function.onFun r f)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq`.

---

The distributional inverse Fourier transform and the classical inverse Fourier transform
coincide on `𝓢(E, F)`.  -/
TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap E F),
  FourierTransformInv.fourierInv ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (FourierTransformInv.fourierInv f)
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
MeasureTheory.Measure.integrable_toReal_rnDeriv : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal) ν
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing bitvector predicates.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceBinPred : Lean.Name → ℕ → ({n : ℕ} → BitVec n → BitVec n → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f))
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f)
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h))
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.indep_congr`. -/
ProbabilityTheory.Kernel.Indep.congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ m₂ _mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → ProbabilityTheory.Kernel.Indep m₁ m₂ η μ
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.objIsoOfEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j : X.I}
  (hij : i = j), X.objIsoOfEq hij = X.objIsoOfEq hij
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- Assume that `A`  is symmetric at real places then, the union of the images of `plusPart`
by `negAt` and of the set of elements of `A` that are zero at at least one real place
is equal to `A`.  -/
NumberField.mixedEmbedding.iUnion_negAt_plusPart_union : ∀ {K : Type u_1} [inst : Field K] (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  (∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun w => ‖x.1 w‖, x.2) ∈ A) →
    (⋃ s, ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A) ∪ A ∩ ⋃ w, {x | x.1 w = 0} = A
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.cons_subst_zero_right : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {f : MvPowerSeries (Fin 2) R} (i j k : σ),
  MvPowerSeries.constantCoeff f = 0 →
    MvPowerSeries.HasSubst ![MvPowerSeries.X i, MvPowerSeries.subst ![MvPowerSeries.X j, MvPowerSeries.X k] f]
-- Mathlib.Order.Grade
Flag.instGradeMaxOrderSubtypeMem : {𝕆 : Type u_1} →
  {α : Type u_3} →
    [inst : PartialOrder α] → [inst_1 : Preorder 𝕆] → [GradeMaxOrder 𝕆 α] → (s : Flag α) → GradeMaxOrder 𝕆 ↥s
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m : M),
  { coeff := fun₀ | n => m } = PolynomialModule.single R n m
-- Lean.Server.ServerTask
Lean.Task.asServerTask : {α : Type u_1} → Task α → Lean.Server.ServerTask α
-- Lean.ReducibilityAttrs
_private.Lean.ReducibilityAttrs.0.Lean.validate : Lean.Name → Lean.ReducibilityStatus → Lean.AttributeKind → Lean.CoreM Unit
-- Init.While
Lean.Loop.forIn : {β : Type u} → {m : Type u → Type v} → [Monad m] → Lean.Loop → β → (Unit → β → m (ForInStep β)) → m β
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1} [inst : SizeOf α]
  [inst_1 : SizeOf β] (inner : Std.ExtDTreeMap α (fun x => β) cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_fdiv_eq_right : ∀ {a b c : ℤ}, b ∣ a → a.fdiv b = c → a = b * c
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Canonical factors are nowhere locally constant zero.
 -/
Complex.meromorphicOrderAt_canonicalFactor_ne_top : ∀ {z : ℂ} {R : ℝ} (w : ℂ), 0 < R → meromorphicOrderAt (Complex.canonicalFactor R w) z ≠ ⊤
-- Mathlib.Order.Hom.Basic
OrderIso.complementedLattice : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [ComplementedLattice α] (f : α ≃o β), ComplementedLattice β
-- Lean.Data.Lsp.Internal
/-- Name of a declaration in a given module.  -/
Lean.Lsp.LeanDeclIdent : Type
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.unitaryGroup.embeddingGL` is the embedding from `Matrix.unitaryGroup n α` to
`LinearMap.GeneralLinearGroup n α`.  -/
Matrix.UnitaryGroup.embeddingGL : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} →
        [inst_2 : CommRing α] →
          [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) →* LinearMap.GeneralLinearGroup α (n → α)
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mem_trivialization_at_source : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) (b : B) (x : E b), ⟨b, x⟩ ∈ (a.pretrivializationAt b).source
-- Mathlib.Algebra.Ring.Aut
/-- Monoid homomorphism from ring automorphisms to additive automorphisms.  -/
RingAut.toAddAut : (R : Type u_1) → [inst : Mul R] → [inst_1 : Add R] → RingAut R →* Multiplicative (AddAut R)
-- Mathlib.GroupTheory.OrderOfElement
charP_of_ne_zero : ∀ {R : Type u_6} [inst : NonAssocRing R] (p : ℕ) [inst_1 : Fintype R],
  Fintype.card R = p → (∀ i < p, ↑i = 0 → i = 0) → CharP R p
-- Mathlib.Algebra.Group.Pi.Units
/-- The monoid equivalence between units of a product,
and the product of the units of each monoid.  -/
MulEquiv.piUnits : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → ((i : ι) → M i)ˣ ≃* ((i : ι) → (M i)ˣ)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_nhdsWithin' : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhdsWithin x s] g → f x = g x → P g s x → P f s x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_setProd : ∀ {α β : Type u} (s : Set α) (t : Set β), Cardinal.mk ↑(s ×ˢ t) = Cardinal.mk ↑s * Cardinal.mk ↑t
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1).left.hom = Y_1.hom
-- Init.Data.List.Lemmas
List.filter_reverse : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l.reverse = (List.filter p l).reverse
-- Lean.Parser.Term
Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_1 : Coe (Lean.TSyntax `Lean.Parser.Term.bracketedBinderF) (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.maxKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.instLinearOrderOfIsOrderedCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α},
  Localization.instLinearOrderOfIsOrderedCancelMonoid =
    { toPartialOrder := Localization.partialOrder, min := fun a b => if a ≤ b then a else b,
      max := fun a b => if a ≤ b then b else a, compare := fun a b => compareOfLessAndEq a b, le_total := ⋯,
      toDecidableLE := Localization.decidableLE, toDecidableEq := Localization.decidableEq,
      toDecidableLT := Localization.decidableLT, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Lean.Meta.Sym.SymM
/-- Runs `x` with the `shareCommon` kernel-projection check disabled.
Use this to wrap code that temporarily violates the `SymM` folded-projections
invariant, e.g., a head reducer that exposes kernel projections in intermediate
terms and restores the invariant in its final result.
 -/
Lean.Meta.Sym.withoutFoldProjsCheck : {m : Type → Type u_1} → {α : Type} → [MonadWithReaderOf Lean.Meta.Sym.Context m] → m α → m α
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q),
  CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.CategoryStruct.comp ((F.mapComp (p' j₁).op.toLoc f₁.op.toLoc).inv.toNatTrans.app (D.obj (α j₁)))
      (CategoryTheory.CategoryStruct.comp
        (D.hom (CategoryTheory.CategoryStruct.comp q p) (CategoryTheory.CategoryStruct.comp f₁ (p' j₁))
          (CategoryTheory.CategoryStruct.comp f₂ (p' j₂)) ⋯ ⋯)
        ((F.mapComp (p' j₂).op.toLoc f₂.op.toLoc).hom.toNatTrans.app (D.obj (α j₂))))
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioc : ∀ (x y : ℝ), Real.toEReal ⁻¹' Set.Ioc ↑x ↑y = Set.Ioc x y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDHashMap.map f m).getKey? k = m.getKey? k
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispanMapIso.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (a : J.R)
  (h_1 : (a : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left a))
  (h_2 : (a : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right a)),
  (match CategoryTheory.Limits.WalkingMultispan.right a with
    | CategoryTheory.Limits.WalkingMultispan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMultispan.right a => h_2 a) =
    h_2 a
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- `QuadraticAlgebra R a b` has a basis over `R` given by `1` and `i`  -/
QuadraticAlgebra.basis : {R : Type u_1} → (a b : R) → [inst : Semiring R] → Module.Basis (Fin 2) R (QuadraticAlgebra R a b)
-- Init.Data.Array.Find
Array.findSome?_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → Option β}, Array.findSome? f #[a] = f a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The property of preserving pullbacks expressed in terms of binary fans.  -/
CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {f : X ⟶ Z} →
              {g : Y ⟶ Z} →
                {h : W ⟶ X} →
                  {k : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) →
                      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k comm) →
                          have this := ⋯;
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) this)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filter f t) k =
      (Option.filter (fun x => f k' x) (Std.ExtDTreeMap.Const.get? t k)).get!
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The sign of the angle between a vector, and a linear combination of that vector with a second
vector, is the sign of the factor by which the second vector is multiplied in that combination
multiplied by the sign of the angle between the two vectors.  -/
Orientation.oangle_sign_smul_add_smul_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ : ℝ),
  (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- A sequence of continuous functions `X → [0,1]` tending to the indicator of a closed set.  -/
IsClosed.apprSeq : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [HasOuterApproxClosed X] → {F : Set X} → IsClosed F → ℕ → BoundedContinuousFunction X NNReal
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_right_eq_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval_one_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
  Polynomial.eval 1 (Polynomial.map f p) = f (Polynomial.eval 1 p)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.brecOn.eq : ∀ {motive : Lean.Grind.CommRing.Poly → Sort u} (t : Lean.Grind.CommRing.Poly)
  (F_1 : (t : Lean.Grind.CommRing.Poly) → Lean.Grind.CommRing.Poly.below t → motive t),
  Lean.Grind.CommRing.Poly.brecOn t F_1 = F_1 t (Lean.Grind.CommRing.Poly.brecOn.go t F_1).2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t : Finset α}, s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_trans : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), ⇑(f.trans g) = ⇑g ∘ ⇑f