mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
snd_integral : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F]
  [CompleteSpace E] {f : X → E × F}, MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_3.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (h : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.Heap.nil h)
  (h_2 : (h : Batteries.BinomialHeap.Imp.Heap α) → motive h Batteries.BinomialHeap.Imp.Heap.nil)
  (h_3 :
    (s₁ : Batteries.BinomialHeap.Imp.Heap α) →
      (r₁ : ℕ) →
        (a₁ : α) →
          (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) →
            (t₁ : Batteries.BinomialHeap.Imp.Heap α) →
              s₁ = Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁ →
                (s₂ : Batteries.BinomialHeap.Imp.Heap α) →
                  (r₂ : ℕ) →
                    (a₂ : α) →
                      (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) →
                        (t₂ : Batteries.BinomialHeap.Imp.Heap α) →
                          s₂ = Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂ →
                            motive (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁)
                              (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂)),
  (h = Batteries.BinomialHeap.Imp.Heap.nil → False) →
    (match h, Batteries.BinomialHeap.Imp.Heap.nil with
      | Batteries.BinomialHeap.Imp.Heap.nil, h => h_1 h
      | h, Batteries.BinomialHeap.Imp.Heap.nil => h_2 h
      | s₁@h:(Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁),
        s₂@h_4:(Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) => h_3 s₁ r₁ a₁ n₁ t₁ h s₂ r₂ a₂ n₂ t₂ h_4) =
      h_2 h
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.toFullSubcategory_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.PrepathObject X.obj) (hQ : P Q.P),
  (Q.toFullSubcategory hQ).p₀ = CategoryTheory.ObjectProperty.homMk Q.p₀
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.isClosed_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsSemitopologicalRing R] (s : Subring R),
  IsClosed ↑s.topologicalClosure
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x =
    PrimeSpectrum.comap (HomogeneousLocalization.mapId 𝒜 ⋯)
      (IsLocalRing.closedPoint (HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the
normed ring satisfies the axiom `‖1‖ = 1`.  -/
tsum_geometric_le_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] (x : R), ‖x‖ < 1 → ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sdiff_div_prod_sdiff : ∀ {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [inst : CommGroup G] [inst_1 : DecidableEq ι] {f : ι → G},
  (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- If `w : TwoSquare T L R B` is a Guitart exact square, and `E` is a pointwise
left Kan extension of `F` along `R`, then `E.compTwoSquare w` is a pointwise left
Kan extension of `T ⋙ F` along `L`.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              {E : R.LeftExtension F} →
                                E.IsPointwiseLeftKanExtension →
                                  (w : CategoryTheory.TwoSquare T L R B) →
                                    [w.GuitartExact] → (E.compTwoSquare w).IsPointwiseLeftKanExtension
-- Mathlib.Analysis.Real.OfDigits
Real.le_sum_ofDigitsTerm_digits : ∀ {x : ℝ} {b : ℕ} [inst : NeZero b],
  x ∈ Set.Ico 0 1 → ∀ (n : ℕ), x - (↑b)⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, Real.ofDigitsTerm (x.digits b) i
-- Mathlib.Order.Defs.LinearOrder
_private.Mathlib.Order.Defs.LinearOrder.0.Ordering.Compares.match_1.eq_2 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.eq, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_2 a b
-- Batteries.Data.String.Lemmas
String.dropWhile_eq : ∀ (p : Char → Bool) (s : String), String.Legacy.dropWhile s p = String.ofList (List.dropWhile p s.toList)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYoneda_hom_app_hom_apply : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCatᵒᵖ)
  (x :
    (CategoryTheory.Limits.Fan.mk
        (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (FintypeCat.toLightProfinite.obj (Opposite.unop X))).pt))
        fun j =>
        F.map ((LightCondensed.fintypeCatAsCofan (FintypeCat.toLightProfinite.obj (Opposite.unop X))).inj j).op).pt)
  (j : ↑(FintypeCat.toLightProfinite.obj (Opposite.unop X)).toTop),
  (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).hom.app X)) x j =
    (CategoryTheory.ConcreteCategory.hom
        (F.map ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj j).op))
      x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.r.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.r S = sInf {c | ∀ (y : ↥S), c 0 (↑y, y)}
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The module topology coming from the action of the topological ring `Rᵐᵒᵖ` on `R`
(via `Semiring.toOppositeModule`, i.e. via `(op r) • m = m * r`) is `R`'s topology.  -/
IsTopologicalSemiring.toOppositeIsModuleTopology : ∀ (R : Type u_1) [inst : Semiring R] [τR : TopologicalSpace R] [IsTopologicalSemiring R], IsModuleTopology Rᵐᵒᵖ R
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- Evaluation of a power series `f` at a point `a`.

It coincides with the evaluation of `f` as a polynomial if `f` is the coercion of a polynomial.
Otherwise, it is only relevant if `φ` is continuous and `a` is topologically nilpotent.  -/
PowerSeries.eval₂ : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Type u_2} → [inst_1 : CommRing S] → (R →+* S) → S → [UniformSpace R] → [UniformSpace S] → PowerSeries R → S
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polarBilin_injective : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N], IsUnit 2 → Function.Injective QuadraticMap.polarBilin
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Ioi_sub_Ioi : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Ioi a) μ →
    a ≤ b → ∫ (x : ℝ) in Set.Ioi a, f x ∂μ - ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg : ∀ (pq : ℤ × ℤ), CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.deg pq = pq.1 + pq.2
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_eq_top : ∀ {M : Type u_2} [inst : Add M] {S : AddSubsemigroup M}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.SetTheory.Ordinal.Basic
/-- Given two ordinals `α < β`, then `principalSegToType α β` is the principal segment embedding
of `α.ToType` into `β.ToType`.  -/
Ordinal.principalSegToType : {α β : Ordinal.{u_1}} → α < β → α.ToType <i β.ToType
-- Batteries.Data.MLList.Basic
/-- Filter a `MLList` using a monadic function.  -/
MLList.filterM : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → m (ULift.{u_1, 0} Bool)) → MLList m α → MLList m α
-- Init.SimpLemmas
implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
-- Mathlib.Logic.Equiv.Set
/-- If `f : α → β` has a left-inverse, then `α` is computably equivalent to the range of `f`.

Note that if `α` is empty, no such `f_inv` exists and so this definition can't be used, unlike
the stronger but less convenient `ofLeftInverse`.  -/
Equiv.ofLeftInverse' : {α : Sort u_3} → {β : Type u_4} → (f : α → β) → (f_inv : β → α) → Function.LeftInverse f_inv f → α ≃ ↑(Set.range f)
-- Mathlib.Algebra.Module.FinitePresentation
Module.isBaseChange_map_of_finite_free : ∀ {R : Type u_5} (N : Type u_6) [inst : CommRing R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] (S : Type u_3)
  (ι : Type u_4) [Finite ι] [inst_4 : CommRing S] [inst_5 : Algebra R S],
  IsBaseChange S (LinearMap.baseChangeHom R S (ι → R) N)
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.apply_wCovBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  f.toRelEmbedding a ⩿ f.toRelEmbedding b ↔ a ⩿ b
-- Lean.Util.Trace
Lean.instExceptToTraceResultExpr : {ε : Type} → Lean.ExceptToTraceResult ε Lean.Expr
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittPow_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m n : ℕ), (WittVector.wittPow p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.Analysis.RCLike.Basic
AddChar.map_neg_eq_conj : ∀ {K : Type u_1} [inst : RCLike K] {G : Type u_3} [Finite G] [inst_2 : AddCommGroup G] (ψ : AddChar G K) (x : G),
  ψ (-x) = (starRingEnd K) (ψ x)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.match_1.congr_eq_4 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁_1 : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var)
  (p₂_1 : Int.Internal.Linear.Poly),
  p₁ = Int.Internal.Linear.Poly.add a₁ x₁ p₁_1 →
    p₂ = Int.Internal.Linear.Poly.add a₂ x₂ p₂_1 →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => h_1 k v p k_1
        | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => h_2 k k_1 v p
        | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_4 a₁ x₁ p₁_1 a₂ x₂ p₂_1
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates finite limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteLimits F.unop] → CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Order.Hom.BoundedLattice
Disjoint.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [inst_3 : OrderBot α] [inst_4 : OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α} (f : F),
  Disjoint a b → Disjoint (f a) (f b)
-- Init.Data.BitVec.Lemmas
/-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`.  -/
BitVec.and_one_eq_setWidth_ofBool_getLsbD : ∀ {w : ℕ} {x : BitVec w}, x &&& 1#w = BitVec.setWidth w (BitVec.ofBool (x.getLsbD 0))
-- Mathlib.Analysis.Complex.Trigonometric
Complex.inv_one_add_tan_sq : ∀ {x : ℂ}, Complex.cos x ≠ 0 → (1 + Complex.tan x ^ 2)⁻¹ = Complex.cos x ^ 2
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsIntegralHom g],
  AlgebraicGeometry.IsIntegralHom (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsIntegralHom f
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_comap'_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : α → β} {f : Filter α} {g : Filter β} {i : γ → α},
  Set.range i ∈ f → (Filter.Tendsto (m ∘ i) (Filter.comap i f) g ↔ Filter.Tendsto m f g)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_τ₃ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH1 f φ).τ₃ = Rep.Hom.toModuleCatHom φ
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_map_equiv_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F]
  {μ : MeasureTheory.Measure E} (L : E ≃L[ℝ] F),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ) ↔ ProbabilityTheory.IsGaussian μ
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_smul : ∀ {m : Type u_3} {n : Type u_4} {R : Type u_2} {α : Type u_1} [inst : SMul α R] (r : α) (A : Matrix m n R),
  (r • A).vec = r • A.vec
-- Mathlib.Order.Atoms
isAtomic_iff_isCoatomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α],
  IsAtomic α ↔ IsCoatomic α
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.existsUnique_from_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {g : Submodule R (E × F)},
  (∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0) → ∀ {a : E}, a ∈ Submodule.map (LinearMap.fst R E F) g → ∃! b, (a, b) ∈ g
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS_nc_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.eq_normS_nc_cert lhs rhs = (lhs.toPolyS_nc == rhs.toPolyS_nc)
-- Mathlib.Analysis.Normed.MulAction
ENormSMulClass.mk : ∀ {α : Type u_3} {β : Type u_4} [inst : ENorm α] [inst_1 : ENorm β] [inst_2 : SMul α β],
  (∀ (r : α) (x : β), ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ) → ENormSMulClass α β
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of a set of additive congruence relations `S`
equals the smallest additive congruence relation containing the binary relation 'there exists
`c ∈ S` such that `x` is related to `y` by `c`'.  -/
AddCon.sSup_eq_addConGen : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), sSup S = addConGen fun x y => ∃ c ∈ S, c x y
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∪ s₂ = s₂ ∪ s₁
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.sectionsAddMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat),
  AddMonCat.sectionsAddMonoid F = (AddMonCat.sectionsAddSubmonoid F).toAddMonoid
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instAddMonoid : {d : ℤ} → AddMonoid (ℤ√d)
-- Init.Data.UInt.Bitwise
UInt64.ofNatLT_and : ∀ (a b : ℕ) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64),
  UInt64.ofNatLT (a &&& b) ⋯ = UInt64.ofNatLT a ha &&& UInt64.ofNatLT b hb
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mkOfUnitCounit`.
This structure won't typically be used anywhere else.
 -/
CategoryTheory.Adjunction.CoreUnitCounit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct a morphism `Grp.mk G ⟶ Grp.mk H` from a  map `f : G ⟶ H` and a `IsMonHom f`
instance.  -/
CategoryTheory.Grp.ofHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : C} →
        [inst_2 : CategoryTheory.GrpObj A] →
          [inst_3 : CategoryTheory.GrpObj B] →
            (f : A ⟶ B) → [CategoryTheory.IsMonHom f] → { X := A, grp := inst_2 } ⟶ { X := B, grp := inst_3 }
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.new : BaseIO Lean.Meta.LazyDiscrTree.ImportData
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The main feature of the Besicovitch Vitali family is that its filter at a point `x` corresponds
to convergence along closed balls. We record one of the two implications here, which will enable us
to deduce specific statements on differentiation of measures in this context from the general
versions.  -/
Besicovitch.tendsto_filterAt : ∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
  [inst_5 : MeasureTheory.SFinite μ] (x : α),
  Filter.Tendsto (fun r => Metric.closedBall x r) (nhdsWithin 0 (Set.Ioi 0)) ((Besicovitch.vitaliFamily μ).filterAt x)
-- Mathlib.RepresentationTheory.FDRep
/-- The monoid homomorphism corresponding to the action of `G` onto `V : FDRep R G`.  -/
FDRep.ρ : {R : Type u} → {G : Type v} → [inst : CommRing R] → [inst_1 : Monoid G] → (V : FDRep R G) → G →* ↑V.V →ₗ[R] ↑V.V
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub_right' : ∀ {n a b c : ℕ}, (a ≤ b ↔ a ≤ c) → b ≡ c [MOD n] → b - a ≡ c - a [MOD n]
-- Std.Time.Format.DateFormat
Std.Time.instInhabitedDayPeriodSymbols.default : Std.Time.DayPeriodSymbols
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_aeval_eq_zero : ∀ (k : Type u) [inst : Field k] {R : Type u_1} [inst_1 : CommSemiring R] [IsAlgClosed k] [inst_3 : Algebra R k]
  [FaithfulSMul R k] (p : Polynomial R), p.degree ≠ 0 → ∃ x, (Polynomial.aeval x) p = 0
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.norm_sq_sdiff_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [inst_5 : DecidableEq ι] (f : (i : ι) → G i) (s₁ s₂ : Finset ι),
      ‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.encard_le_eRank : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I.encard ≤ M.eRank
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {x : WithAbs v}, x.ofAbs = 0 ↔ x = 0
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.comp_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {x y z : C} (f : x ⟶ y)
  (g : y ⟶ z), W.multiplicativeClosure f → W g → W.multiplicativeClosure (CategoryTheory.CategoryStruct.comp f g)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.erase ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        ⟨{ size := size - 1, buckets := buckets'.uset i (Std.DHashMap.Internal.AssocList.erase a bkt) ⋯ }, ⋯⟩
      else ⟨{ size := size, buckets := buckets }, hm⟩
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
ContinuousMap.UniqueHom.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A], ContinuousMap.UniqueHom R A = ContinuousMap.UniqueHom R A
-- Mathlib.Algebra.Homology.Opposite
imageToKernel_unop : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Abelian V] {X Y Z : Vᵒᵖ}
  (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0),
  imageToKernel g.unop f.unop ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop
        (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_erase : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.erase n p).support = p.support.erase n
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_right : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) (P : CategoryTheory.Functor C₀ᵒᵖ A) (j : data.multicospanShape.R),
  (data.multicospanIndex P).right j = P.obj (Opposite.op (data.Y j.snd))
-- Init.Data.Fin.Lemmas
Fin.succ_succ_ne_one : ∀ {n : ℕ} (a : Fin n), a.succ.succ ≠ 1