mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.Equivalence.congrFullSubcategory_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D)
  [inst_2 : Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P),
  (e.congrFullSubcategory h).counitIso =
    (Q.fullyFaithfulι.whiskeringRight Q.FullSubcategory).preimageIso (Q.ι.isoWhiskerLeft e.counitIso)
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.instInhabitedEqnInfo.default : Lean.Elab.Structural.EqnInfo
-- Std.Data.DTreeMap.Raw.Basic
/-- Internal implementation detail of the tree map.  -/
Std.DTreeMap.Raw.WF.out : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.WF → t.inner.WF
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_apply_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : E → 𝕜},
  Function.HasTemperateGrowth g → ∀ (f : SchwartzMap E F) (x : E), ((SchwartzMap.smulLeftCLM F g) f) x = g x • f x
-- Init.Data.List.Perm
List.perm_append_right_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Perm (l₂ ++ l) ↔ l₁.Perm l₂
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y),
  ∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.map_bounded' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (self : BoundedContinuousFunction α β), ∃ C, ∀ (x y : α), dist (self.toFun x) (self.toFun y) ≤ C
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j)
      (CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv =
    CategoryTheory.CategoryStruct.comp (w.inv.app j) (CategoryTheory.Limits.colimit.ι F j)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.mem_map_iff_mem_of_injective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁},
  Function.Injective ⇑f → (f x ∈ AffineSubspace.map f s ↔ x ∈ s)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.diff_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.diff m₂ = m₁ \ m₂
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.instInhabitedEvent.default : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Grind.Linarith.Poly.div : Lean.Grind.Linarith.Poly → ℤ → Lean.Grind.Linarith.Poly
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_if : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {x : β} {t : Set β} {s : Set α}
  [inst : Decidable (x ∈ t)], μ (if x ∈ t then s else ∅) = t.indicator (fun x => μ s) x
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStronglyProgressive.stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.noConfusionType : Sort v✝ → Lean.Lsp.SignatureHelpTriggerKind → Lean.Lsp.SignatureHelpTriggerKind → Sort v✝
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAt_sub_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt (fun x => f x - c) f' x ↔ HasDerivAt f f' x
-- Mathlib.Analysis.Convex.Hull
convexHull_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (a : 𝕜) (s : Set E), (convexHull 𝕜) (a • s) = a • (convexHull 𝕜) s
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_div : ∀ {a b c d : ENNReal}, a ≤ b → d ≤ c → a / c ≤ b / d
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj (Opposite.unop X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map
        (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f).unop)
      h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y).unop
      (CategoryTheory.CategoryStruct.comp f.unop h)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.instIsLocalRingMaximalIdealOfIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R],
  IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinallySmall.preservesColimitsOfShape_of_isFiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.FinallySmall C] {D : Type u_1} {E : Type u_2}
  [inst_4 : CategoryTheory.Category.{v_1, u_1} D] [inst_5 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v_1, v_2, u_1, u_2} F],
  CategoryTheory.Limits.PreservesColimitsOfShape C F
-- Mathlib.Algebra.Order.IsBotOne
NeZero.of_gt : ∀ {α : Type u_1} {a b : α} [inst : Zero α] [inst_1 : Preorder α] [IsBotZeroClass α], a < b → NeZero b
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.reₗ_apply : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] (self : QuadraticAlgebra R a b),
  (QuadraticAlgebra.reₗ a b) self = self.re
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instIterator.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Std.IteratorAccess α m]
  [inst_2 : Monad m],
  Std.Iterators.Types.StepSizeIterator.instIterator =
    {
      IsPlausibleStep := fun it step =>
        Std.IterM.IsPlausibleNthOutputStep it.internalState.nextIdx it.internalState.inner
            (Std.IterStep.mapIterator (Std.Iterators.Types.StepSizeIterator.inner ∘ Std.IterM.internalState) step) ∧
          ∀ (it' : Std.IterM m β) (out : β),
            step = Std.IterStep.yield it' out →
              it'.internalState.n = it.internalState.n ∧ it'.internalState.nextIdx = it.internalState.n,
      step := fun it =>
        (fun s =>
            Std.Shrink.deflate
              ⟨Std.IterStep.mapIterator
                  (fun x => { internalState := { nextIdx := it.internalState.n, n := it.internalState.n, inner := x } })
                  ↑s,
                ⋯⟩) <$>
          it.internalState.inner.nextAtIdx? it.internalState.nextIdx }
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_xor_distrib : ∀ {i a b : ℕ}, (a ^^^ b) <<< i = a <<< i ^^^ b <<< i
-- Lean.MetavarContext
/-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext`.
We also use it for pretty printing anonymous metavariables.  -/
Lean.MetavarDecl.index : Lean.MetavarDecl → ℕ
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.uniformContinuous : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'},
  v.IsEquiv w → UniformContinuous ⇑(RingHom.id R)
-- Lean.Meta.Basic
/-- If diagnostics are enabled, record that `declName` has been unfolded.  -/
Lean.Meta.recordUnfold : Lean.Name → Lean.MetaM Unit
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.toFullSubcategory_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.Precylinder X.obj) (hQ : P Q.I),
  (Q.toFullSubcategory hQ).i₁ = CategoryTheory.ObjectProperty.homMk Q.i₁
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.inter_eq_right_of_subset : ∀ {x y : ZFSet.{u}}, y ⊆ x → x ∩ y = y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖
-- Mathlib.Order.Bounds.Defs
/-- A set `s` is said to be cofinal for a set `t` if, for all `a ∈ s` there exists `b ∈ t`
such that `a ≤ b`.  -/
IsCofinalFor : {α : Type u_1} → [LE α] → Set α → Set α → Prop
-- Mathlib.Analysis.Fourier.AddCircle
/-- The family of exponential monomials `fun x => exp (2 π i n x / T)`, parametrized by `n : ℤ` and
considered as bundled continuous maps from `ℝ / ℤ • T` to `ℂ`.  -/
fourier : {T : ℝ} → ℤ → C(AddCircle T, ℂ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_div_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s / t).sup f = t.sup fun y => s.sup fun x => f (x / y)
-- Mathlib.Algebra.Algebra.ZMod
ZMod.instIsScalarTower : ∀ (n : ℕ) (R : Type u_2) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module (ZMod n) R]
  [m₁ : Module (ZMod n) M] [inst_3 : Module R M], IsScalarTower (ZMod n) R M
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f pf s x r →
    HasFPowerSeriesWithinOnBall g pg s x r → HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s x r
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- The canonical isomorphism between `presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F`
and `(whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B` when `F : A ⥤ B`
preserves sheafification.  -/
CategoryTheory.presheafToSheafCompComposeAndSheafifyIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                [inst_3 : CategoryTheory.HasWeakSheafify J B] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                    [J.PreservesSheafification F] →
                      (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F) ≅
                        ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp
                          (CategoryTheory.presheafToSheaf J B)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basisSet.congr_simp : ∀ {ι : Type u_3} {s s_1 : Set (ι → ℕ)} (e_s : s = s_1) (hs : IsProperLinearSet s) [inst : Finite ι] (a a_1 : ι → ℕ),
  a = a_1 → IsProperLinearSet.basisSet✝ hs a = IsProperLinearSet.basisSet✝ ⋯ a_1
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.BisimO.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) (a : α) (s : Stream'.Seq α)
  (a' : α) (s' : Stream'.Seq α) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_1 : Option (Stream'.Seq1 α)) → motive x x_1),
  (match some (a, s), some (a', s') with
    | none, none => h_1 ()
    | some (a, s), some (a', s') => h_2 a s a' s'
    | x, x_1 => h_3 x x_1) =
    h_2 a s a' s'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.mk.injEq : ∀ (name : String) (kind : Lean.Lsp.SymbolKind) (tags? : Option (Array Lean.Lsp.SymbolTag)) (detail? : Option String)
  (uri : Lean.Lsp.DocumentUri) (range selectionRange : Lean.Lsp.Range) (data? : Option Lean.Json) (name_1 : String)
  (kind_1 : Lean.Lsp.SymbolKind) (tags?_1 : Option (Array Lean.Lsp.SymbolTag)) (detail?_1 : Option String)
  (uri_1 : Lean.Lsp.DocumentUri) (range_1 selectionRange_1 : Lean.Lsp.Range) (data?_1 : Option Lean.Json),
  ({ name := name, kind := kind, tags? := tags?, detail? := detail?, uri := uri, range := range,
        selectionRange := selectionRange, data? := data? } =
      { name := name_1, kind := kind_1, tags? := tags?_1, detail? := detail?_1, uri := uri_1, range := range_1,
        selectionRange := selectionRange_1, data? := data?_1 }) =
    (name = name_1 ∧
      kind = kind_1 ∧
        tags? = tags?_1 ∧
          detail? = detail?_1 ∧ uri = uri_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1 ∧ data? = data?_1)
-- Mathlib.Control.Traversable.Basic
LawfulTraversable.mk : ∀ {t : Type u → Type u} [inst : Traversable t] [toLawfulFunctor : LawfulFunctor t],
  (∀ {α : Type u} (x : t α), traverse pure x = pure x) →
    (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
        [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α),
        traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)) →
      (∀ {α β : Type u} (f : α → β) (x : t α), traverse (pure ∘ f) x = pure (f <$> x)) →
        (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
            [LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α),
            (fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x) →
          LawfulTraversable t
-- Mathlib.Util.Notation3
/-- `notation3` argument simulating a Lean 3 fold notation.  -/
Mathlib.Notation3.foldAction : Lean.ParserDescr
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.hasSum_one_poissonMeasure : ∀ (r : NNReal), HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1
-- Init.Data.Option.Lemmas
Option.max_eq_left_of_lt : ∀ {α : Type u_1} [inst : LT α] [inst_1 : Max α],
  (∀ (x y : α), x < y → x ⊔ y = y) → ∀ {a b : Option α}, a < b → a ⊔ b = b
-- Init.Classical
Classical.decide_not : ∀ (p : Prop) [inst : Decidable ¬p], (decide ¬p) = !decide p
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.sub_bind : ∀ {α β : Type u} (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α), x - y >>= f = (x >>= f) - (y >>= f)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {Z : C} (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (L.iCycles i) h) =
    CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (φ.f i) h)
-- Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
instFreeCarrierX₂ModuleCatProjectiveShortComplex : ∀ {R : Type u} [inst : Ring R] [inst_1 : Small.{v, u} R] (M : ModuleCat R), Module.Free R ↑M.projectiveShortComplex.X₂
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.instOne : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → One (GroupLike R A)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_ge_of_const_le_real : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {s : Set X} {f : X → ℝ} {c : ℝ},
  MeasurableSet s →
    μ s ≠ ⊤ → (∀ x ∈ s, c ≤ f x) → MeasureTheory.IntegrableOn (fun x => f x) s μ → c * μ.real s ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sections_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {s t : M.sections}, s = t ↔ ∀ (X : Cᵒᵖ), ↑s X = ↑t X
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onTerm.eq_2 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') (l : ℕ) (_f : L.Functions l)
  (ts : Fin l → L.Term α),
  φ.onTerm (FirstOrder.Language.func _f ts) = FirstOrder.Language.func (φ.onFunction _f) fun i => φ.onTerm (ts i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom
      CategoryTheory.Limits.prod.fst =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
      CategoryTheory.Limits.prod.fst
-- Mathlib.Topology.Gluing
TopCat.GlueData.ofOpenSubsets_toGlueData_f : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α)
  (i j :
    { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i),
        V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
        t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
        t_inter := ⋯, cocycle := ⋯ }.J),
  (TopCat.GlueData.ofOpenSubsets U).f i j = ((TopologicalSpace.Opens.map (U i).inclusion').obj (U j)).inclusion'
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Array.unattach_filter_eq_if : ∀ {α : Type u} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool},
  (Array.filter f xs).unattach = Array.filter (fun x => if h : p x then f ⟨x, h⟩ else false) xs.unattach
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_copy : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndunion_le_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndunion t ≤ s ∪ t
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- Theorems about `padicNormE` are named with a `'` so the names do not conflict with the
equivalent theorems about `norm` (`‖ ‖`).  -/
padicNormE.nonarchimedean' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (q r : ℚ_[p]), padicNormE (q + r) ≤ max (padicNormE q) (padicNormE r)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_injective : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R], Function.Injective MvPolynomial.X
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqFunDecl : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.FunDecl pu)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.values_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.values = t₂.values
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
_private.Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex.0.SSet.Subcomplex.Pairing.RankFunction.isPushout_aux₂ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι}, Function.Injective f.mapN
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
InnerProductGeometry.sin_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y ≠ 0 → Real.sin (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x + y‖
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le_aleph0 : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c ≤ Cardinal.aleph0 ↔ c ≤ Cardinal.aleph0
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The orbit of an element under an action.  -/
AddAction.orbit : (γ : Type u_2) → {α : Type u_3} → [VAdd γ α] → α → Set α
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.evalList.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (x : ℕ) → motive [x])
  (h_3 : (x : ℕ) → (xs : List ℕ) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: xs => h_3 x xs) =
    h_1 ()
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
_private.Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum.0.ZMod.χ₄.match_1.eq_4 : ∀ (motive : ZMod 4 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 1)
  (h_4 : Unit → motive 3),
  (match 3 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 1 => h_3 ()
    | 3 => h_4 ()) =
    h_4 ()
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₁_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₁.map f = f.τ₁
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A partial iso is an `S`-map if the underlying morphism is.  -/
AlgebraicGeometry.Scheme.PartialIso.IsOver : {X Y S : AlgebraicGeometry.Scheme} → (X ⟶ S) → (Y ⟶ S) → X.PartialIso Y → Prop
-- Mathlib.RepresentationTheory.Invariants
/-- The `averageMap` sends elements of `V` to the subspace of invariants.
 -/
Representation.averageMap_invariant : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)] (v : V),
  ρ.averageMap v ∈ ρ.invariants
-- Init.Data.List.Perm
List.Perm.sum_nat : ∀ {l₁ l₂ : List ℕ}, l₁.Perm l₂ → l₁.sum = l₂.sum