mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_neg : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.MemLp f p μ),
  MeasureTheory.MemLp.toLp (-f) ⋯ = -MeasureTheory.MemLp.toLp f hf
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ioo_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (c - b) (d - b)
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindIso_hom_hom_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S),
  (Rep.Hom.hom A.indCoindIso.hom).toLinearMap = A.indToCoind
-- Mathlib.SetTheory.ZFC.Basic
/-- The union operator, the collection of elements of elements of a ZFC set. Uses `⋃₀` notation,
scoped under the `ZFSet` namespace.
 -/
ZFSet.sUnion : ZFSet.{u_1} → ZFSet.{u_1}
-- Lean.Elab.ConfigEval.DeriveEvalTerm
/-- Resolves `id`, making sure the result is in namespace `c`.
Returns `s` if the resolved name is of the form of the form `Name.str c s`.
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalTerm.0.Lean.Elab.ConfigEval.EvalTerm.resolveAtomicNameForConstNamespace : Lean.Name → Lean.Ident → Lean.Elab.TermElabM String
-- Mathlib.RingTheory.Coalgebra.Basic
/-- A coalgebra `A` is cocommutative if its comultiplication `δ : A → A ⊗ A` commutes with the
swapping `β : A ⊗ A ≃ A ⊗ A` of the factors in the tensor product.  -/
Coalgebra.IsCocomm : (R : Type u) →
  (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → Prop
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  {P : F.ObjectProperty},
  (∀ {X Y : B} {M : ↑(F.obj X)}, P.prop X M → ∀ (f : X ⟶ Y), P.prop Y ((F.map f).toFunctor.obj M)) →
    P.IsClosedUnderMapObj
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.foldlM f init t = Array.foldlM (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.snd_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η], (κ.prod η).snd = η
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.ι_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j)
      (CategoryTheory.Limits.chosenCoend.map f) =
    CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j) (CategoryTheory.Limits.chosenCoend.ι G j)
-- Mathlib.Data.Finset.Card
/-- Suppose that, given objects defined on all strict subsets of any finset `s`, one knows how to
define an object on `s`. Then one can inductively define an object on all finsets, starting from
the empty set and iterating. This can be used either to define data, or to prove properties.  -/
Finset.strongInduction : {α : Type u_1} →
  {p : Finset α → Sort u_4} → ((s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) → (s : Finset α) → p s
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_nsmul : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f : X ⟶ Y} {n : ℕ},
  F.map (n • f) = n • F.map f
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_div : ∀ (a b : BitVec 32), { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousMapClass.map_bounded : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : TopologicalSpace α}
  {inst_1 : PseudoMetricSpace β} {inst_2 : FunLike F α β} [self : BoundedContinuousMapClass F α β] (f : F),
  ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.inclusion_apply_coe : ∀ {V : Type u} {G : SimpleGraph V} {x y : G.Subgraph} (h : x ≤ y) (v : ↑x.verts),
  ↑((SimpleGraph.Subgraph.inclusion h) v) = ↑v
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.neg_coeffs : ∀ {l : Lean.Omega.LinearCombo}, (-l).coeffs = -l.coeffs
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.instHasFunctorialFactorizationLlpRlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [I.HasSmallObjectArgument], I.rlp.llp.HasFunctorialFactorization I.rlp
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.memLp_finsetSum' : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  (s : Finset ι) {f : ι → α → ε'}, (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) → MeasureTheory.MemLp (∑ i ∈ s, f i) p μ
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.toQuotientPaths_obj_as : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), ((CategoryTheory.toQuotientPaths C).obj X).as = X
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Isosceles Triangle Theorem**: Pons asinorum, angle-at-point form.  -/
EuclideanGeometry.angle_eq_angle_of_dist_eq : ∀ {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},
  dist p₁ p₂ = dist p₁ p₃ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₃ p₂
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_of_empty : ∀ {α : Type u_4} [inst : Fintype α] [inst_1 : IsEmpty α] {β : α → Type u_5} {m : (a : α) → MeasurableSpace (β a)}
  (μ : (a : α) → MeasureTheory.Measure (β a)) (x : optParam ((a : α) → β a) fun a => isEmptyElim a),
  MeasureTheory.Measure.pi μ = MeasureTheory.Measure.dirac x
-- Mathlib.Topology.Sheaves.Flasque
TopCat.Presheaf.IsFlasque.epi : ∀ {X : TopCat} {C : Type v} {inst : CategoryTheory.Category.{w, v} C} {F : TopCat.Presheaf C X} [self : F.IsFlasque]
  {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V), CategoryTheory.Epi (F.map i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeFormAux_changeFormAux : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (B : LinearMap.BilinForm R M) (v : M) (x : CliffordAlgebra Q),
  ((CliffordAlgebra.changeFormAux Q B) v) (((CliffordAlgebra.changeFormAux Q B) v) x) = (Q v - (B v) v) • x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Given a right homology data `h` of a short complex `S`, we can construct another right homology
data by choosing another cokernel and kernel that are isomorphic to the ones in `h`.  -/
CategoryTheory.ShortComplex.RightHomologyData.copy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → {Q' H' : C} → (Q' ≅ h.Q) → (H' ≅ h.H) → S.RightHomologyData
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.toArray_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m], (Std.IterM.empty m β).toArray = pure #[]
-- Lean.Elab.Arg
Lean.Elab.Term.instToMessageDataArg : Lean.ToMessageData Lean.Elab.Term.Arg
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.crlfToLf.go.eq_def : ∀ (text acc : String) (accStop pos : String.Pos.Raw),
  String.crlfToLf.go✝ text acc accStop pos =
    if h : String.Pos.Raw.atEnd text pos = true then
      if accStop = 0 then text else acc ++ String.Pos.Raw.extract text accStop pos
    else
      let c := String.Pos.Raw.get' text pos h;
      let pos' := String.Pos.Raw.next' text pos h;
      if h' :
          ¬String.Pos.Raw.atEnd text pos' = true ∧
            (c == '\x0d') = true ∧ (String.Pos.Raw.get text pos' == '\n') = true then
        have acc := acc ++ String.Pos.Raw.extract text accStop pos;
        String.crlfToLf.go✝ text acc pos' (String.Pos.Raw.next' text pos' ⋯)
      else String.crlfToLf.go✝ text acc accStop pos'
-- Mathlib.Algebra.Jordan.Basic
/-- Semigroup multiplication satisfies the (non-commutative) Jordan axioms  -/
Semigroup.isJordan : ∀ (A : Type u_1) [inst : Semigroup A], IsJordan A
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsMap_continuous : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f : α → β} (h : Continuous f),
  Continuous h.connectedComponentsMap
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_mono : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], Monotone NNRat.cast
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- The preimage of a proper space under a Lipschitz proper map is proper.  -/
LipschitzWith.properSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] [ProperSpace Y] {f : X → Y},
  IsProperMap f → ∀ {K : NNReal}, LipschitzWith K f → ProperSpace X
-- Init.Grind.Tactics
/-- `grobner` solves goals that can be phrased as polynomial equations (with further polynomial equations as hypotheses)
over commutative (semi)rings, using the Grobner basis algorithm.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `grobner` solver.
Please use `grind` instead if you need additional capabilities.
 -/
Lean.Parser.Tactic.grobner : Lean.ParserDescr
-- Lean.Elab.Match
Lean.Elab.Term.Discr.expr : Lean.Elab.Term.Discr → Lean.Expr
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.equivHom_injective : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [Finite G] [Nontrivial k],
  Function.Injective ⇑(TannakaDuality.FiniteGroup.equivHom k G)
-- Mathlib.GroupTheory.Congruence.Defs
/-- Congruence relations are symmetric.  -/
Con.symm : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {x y : M}, c x y → c y x
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp S.homologyπ
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv =
    CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv π
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], (↑p).valuation = 1
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimit_zero_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (j : J), 0 = AddGrpCat.FilteredColimits.G.mk F ⟨j, 0⟩
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_eq_zero_of_eq : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) {i j : ι},
  v i = v j → i ≠ j → f v = 0
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Array α → Sort u_2) (head : α) (tail : List α) (x : Array α)
  (h_1 : (x x_1 : ℕ) → (x_2 : Array α) → motive [] x x_1 x_2)
  (h_2 : (head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc),
  (match head :: tail, 0, 0, x with
    | [], x, x_1, x_2 => h_1 x x_1 x_2
    | head :: tail, 0, 0, x => h_2 head tail x
    | a :: xs, 0, i.succ, acc => h_3 a xs i acc
    | a :: xs, i.succ, 0, acc => h_4 a xs i acc
    | a :: xs, i.succ, j.succ, acc => h_5 a xs i j acc) =
    h_2 head tail x
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_eq_zero_iff_of_nonneg : ∀ {ι : Type u_9} {M : Type u_10} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M] [AddLeftMono M]
  {f : ι → M}, 0 ≤ f → (∑ i, f i = 0 ↔ f = 0)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Given a limit cone for the family `f : J → (X ⟶ Y)`, for any `Z`, morphisms from `Z` to its point
are in bijection with morphisms `h : Z ⟶ X` such that `∀ j₁ j₂, h ≫ f j₁ = h ≫ f j₂`.
Further, this bijection is natural in `Z`: see `Trident.Limits.homIso_natural`.
 -/
CategoryTheory.Limits.Trident.IsLimit.homIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {t : CategoryTheory.Limits.Trident f} →
              CategoryTheory.Limits.IsLimit t →
                (Z : C) →
                  (Z ⟶ t.pt) ≃
                    { h //
                      ∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }
-- Mathlib.Combinatorics.Optimization.ValuedCSP
ValuedCSP.Term.mk : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] →
          {Γ : ValuedCSP D C} → {ι : Type u_3} → (n : ℕ) → (f : (Fin n → D) → C) → ⟨n, f⟩ ∈ Γ → (Fin n → ι) → Γ.Term ι
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_add_const : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f : α → M} (C : M), Filter.Tendsto (fun x => f x + C) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.inclusionSpan_apply_coe : ∀ {R : Type u_1} {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (p : Submodule R M)
  (x : ↥p), ↑((Submodule.inclusionSpan S p) x) = ↑x
-- Lean.Server.Requests
Lean.Server.RequestHandler.fileSource : Lean.Server.RequestHandler → Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MonotoneOn.memLp_isCompact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact s → MonotoneOn f s → MeasureTheory.MemLp f p (μ.restrict s)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.coconeTypesEquiv_symm_apply_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  (c : CategoryTheory.Limits.Cocone F), (F.coconeTypesEquiv.symm c).pt = c.pt
-- Mathlib.Control.Fold
Monoid.Foldl.get.eq_1 : ∀ {α : Type u} (x : Monoid.Foldl α), x.get = ⇑(CategoryTheory.ConcreteCategory.hom (MulOpposite.unop x))
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorMapObj.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : 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} C₃]
  (F F_1 : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (e_F : F = F_1) {I : Type u_4} {J : Type u_5}
  {K : Type u_6} (p p_1 : I × J → K) (e_p : p = p_1) (X X_1 : CategoryTheory.GradedObject I C₁) (e_X : X = X_1)
  (Y Y_1 : CategoryTheory.GradedObject J C₂) (e_Y : Y = Y_1)
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] (a a_1 : K),
  a = a_1 →
    CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y a =
      CategoryTheory.GradedObject.mapBifunctorMapObj F_1 p_1 X_1 Y_1 a_1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- This lemma uses the simp-normal form `⇑T ∘ ⇑(T†)` instead of `⇑(T ∘L T†)`
(note the difference between `∘` and `∘L`).
You may need to rewrite with `ContinuousLinearMap.coe_comp'` before applying this lemma.
 -/
ContinuousLinearMap.self_comp_adjoint_injective_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  Function.Injective (⇑T ∘ ⇑(ContinuousLinearMap.adjoint T)) ↔ Function.Injective ⇑(ContinuousLinearMap.adjoint T)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed iff it is the integral closure of itself in its field of fractions.  -/
isIntegrallyClosed_iff_isIntegralClosure : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsIntegrallyClosed R ↔ IsIntegralClosure R R K
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_eq_one : ∀ {α : Type u} [inst : One α] {a : α}, ↑a = 1 ↔ a = 1
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Equation (11.3.8) from Cohn's proof, viewed as an equation of bivariate polynomials.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₁_mul_Φ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  RatFunc.Luroth.Q₁✝ h * RatFunc.Luroth.Φ✝ E = RatFunc.Luroth.θ✝ E
-- Mathlib.RingTheory.Ideal.IsAugmentation
/-- If `S` is a subalgebra of an `R`-algebra `A`, then an ideal `I`of `A` is an augmentation ideal
for the `R`-algebra structure
if and only if it is an augmentation ideal for the `S`-algebra structure.  -/
Ideal.isAugmentation_subalgebra_iff : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_2} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {S : Subalgebra R A} {I : Ideal A},
  Ideal.IsAugmentation (↥S) I ↔ IsCompl (Subalgebra.toSubmodule S) (Submodule.restrictScalars R I)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.truncGELT a b ⟶ t.truncLTGE a b`
(which is an isomorphism, see `truncGELTIsoLTGE`.)  -/
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] → (a b : ℤ) → t.truncGELT a b ⟶ t.truncLTGE a b
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_sup_of_normal_left' : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  IsPGroup p ↥H → IsPGroup p ↥K → K ≤ Subgroup.normalizer ↑H → IsPGroup p ↥(H ⊔ K)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.digamma_apply_add_one : ∀ (s : ℂ), (∀ (m : ℕ), s ≠ -↑m) → (s + 1).digamma = s.digamma + s⁻¹
-- Aesop.Tree.Data
Aesop.GoalState.unknown.sizeOf_spec : sizeOf Aesop.GoalState.unknown = 1
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.Finite.to_noetherianSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Finite α], TopologicalSpace.NoetherianSpace α
-- Init.Data.Array.Lemmas
Array.contains_reverse : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {x : α}, xs.reverse.contains x = xs.contains x
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Additive submonoids of an additive monoid `Additive M` are isomorphic to submonoids of `M`.  -/
AddSubmonoid.toSubmonoid' : {M : Type u_1} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
-- Mathlib.Tactic.NormNum.Basic
/-- If `b` divides `a` and `a` is invertible, then `b` is invertible.  -/
Mathlib.Meta.NormNum.invertibleOfMul' : {α : Type u_1} → [inst : Semiring α] → {a k b : ℕ} → [Invertible ↑a] → a = k * b → Invertible ↑b
-- Mathlib.Order.BoundedOrder.Basic
ULift.instBot : {α : Type u} → [Bot α] → Bot (ULift.{v, u} α)
-- Init.MetaTypes
Lean.Module.mk.injEq : ∀ (header : Lean.Syntax) (commands : Array Lean.Syntax) (header_1 : Lean.Syntax) (commands_1 : Array Lean.Syntax),
  ({ header := header, commands := commands } = { header := header_1, commands := commands_1 }) =
    (header = header_1 ∧ commands = commands_1)
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $r_2 (r_1 r_2)^m x$, where $m$ is a natural number.  -/
Module.reflection_mul_reflection_mul_reflection_pow_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_mul_reflection_pow_apply_self._auto_1 →
    (Module.reflection hg * (Module.reflection hf * Module.reflection hg) ^ m) x =
      (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) + Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1))) • x +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) * -g x) • y
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.step_iter : ∀ {β : Type w} {n : ℕ} {xs : Vector β n},
  xs.iter.step =
    if h : 0 < n then Std.PlausibleIterStep.yield (xs.iterFromIdx 1) xs[0] ⋯ else Std.PlausibleIterStep.done ⋯
-- Std.Sync.CancellationToken
/-- The cancellation reason if cancelled, none otherwise.
 -/
Std.CancellationToken.State.reason : Std.CancellationToken.State → Option Std.CancellationReason
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toExpr : FBinopElab.Tree✝ → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Batteries.Lean.AttributeExtra
/-- `TagAttributeExtra` works around a limitation of `TagAttribute`, which is that definitions
must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied
in the same file as the declaration: During the declaration of the attribute itself,
we can tag arbitrary other definitions, but once the attribute is declared we must tag things
in the same file as normal.
 -/
Lean.TagAttributeExtra : Type