mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_star_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u : ↥(unitary R)) (x : R),
  ((Unitary.conjStarAlgAut S R) (star u)) x = star ↑u * x * ↑u
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instCommSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : CommSemiring α] →
      [inst_1 : PartialOrder α] →
        [CanonicallyOrderedAdd α] → [NoZeroDivisors α] → [Nontrivial α] → CommSemiring (WithBot α)
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.toMeasurableEquiv.congr_simp : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] (f f_1 : E ≃ₗᵢ[ℝ] F),
  f = f_1 → f.toMeasurableEquiv = f_1.toMeasurableEquiv
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  [inst_2 : Inhabited (β k)],
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getValueCast! k (Std.Internal.List.eraseKey k l) = default
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.mul_smul_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.ModObj.smul) CategoryTheory.ModObj.smul)
-- Mathlib.RingTheory.Teichmuller
Perfection.coe_teichmuller_eq_teichmuller₀ : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], ⇑(Perfection.teichmuller p I) = ⇑(Perfection.teichmuller₀ p I)
-- Lean.Elab.Exception
Lean.Elab.throwAutoBoundImplicitLocal : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadExceptOf Lean.Exception m] → Lean.Name → m α
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) ⁻¹' Set.Ioo b c = Set.Ioo (b * a) (c * a)
-- Mathlib.Computability.EpsilonNFA
NFA.toεNFA_evalFrom_match : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (start : Set σ), M.toεNFA.evalFrom start = M.evalFrom start
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.writeNotification : {α : Type u_1} → [Lean.ToJson α] → Lean.JsonRpc.Notification α → Lean.Lsp.Ipc.IpcM Unit
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso_hom_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D}
  (h : CategoryTheory.Abelian.coimage (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f)) h
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_getElem : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  pat ≠ "" →
    (String.Slice.Pattern.Model.MatchesAt pat pos ↔
      ∃ (h : pos.offset.byteIdx + pat.toByteArray.size ≤ s.copy.toByteArray.size),
        ∀ (j : ℕ) (hj : j < pat.toByteArray.size), pat.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j])
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.mapDomainRingHom.eq_1 : ∀ {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [inst : Semiring β] [inst_1 : Monoid α]
  [inst_2 : Monoid α₂] [inst_3 : FunLike F α α₂] [inst_4 : MulSemiringAction α β] [inst_5 : MulSemiringAction α₂ β]
  [inst_6 : MonoidHomClass F α α₂] {f : F} (hf : ∀ (a : α) (x : β), a • x = f a • x),
  SkewMonoidAlgebra.mapDomainRingHom hf =
    { toFun := (↑(SkewMonoidAlgebra.mapDomain ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_coe : ∀ {α : Type u_2} {β : Type u_3} (s : Finset α) (t : α → Set β), ⋃ x ∈ ↑s, t x = ⋃ x ∈ s, t x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').hom
      (CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f g) g'
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.sheafify Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (J.toSheafify Q) h) =
    CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) h)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  {t₁ t₂ : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)} {f : t₁ ⟶ t₂},
  (CategoryTheory.WithTerminal.coneEquiv.inverse.map f).hom.left = f.hom
-- Mathlib.RingTheory.PrincipalIdealDomain
gcd_isUnit_iff : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] [inst_3 : GCDMonoid R] (x y : R),
  IsUnit (gcd x y) ↔ IsCoprime x y
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (a : A), ↑e a = e a
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.mul_eq_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanHom 2 A B f → ∀ {a b c d : α}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a * b = c * d → f a * f b = f c * f d
-- Mathlib.GroupTheory.Perm.Basic
Set.MapsTo.perm_pow : ∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.MapsTo (⇑f) s s → ∀ (n : ℕ), Set.MapsTo (⇑(f ^ n)) s s
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M` and a Localization map `f : M →* N` away from `x`, we get an isomorphism between
the Localization of `M` at the Submonoid generated by `x` as a quotient type and `N`.  -/
Localization.Away.mulEquivOfQuotient : {M : Type u_1} →
  [inst : CommMonoid M] →
    {N : Type u_2} →
      [inst_1 : CommMonoid N] → (x : M) → Submonoid.LocalizationMap.AwayMap x N → Localization.Away x ≃* N
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsStrictlyPositive.of_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  IsStrictlyPositive a → a ≤ b → IsStrictlyPositive b
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.prodMk : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {M' : Type u_3} [inst_1 : One M'] {f : α → M} {g : α → M'},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun a => (f a, g a)
-- Mathlib.Order.RelSeries
RelSeries.mk.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (length : ℕ) (toFun toFun_1 : Fin (length + 1) → α) (e_toFun : toFun = toFun_1)
  (step : ∀ (i : Fin length), (toFun i.castSucc, toFun i.succ) ∈ r),
  { length := length, toFun := toFun, step := step } = { length := length, toFun := toFun_1, step := ⋯ }
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.String.Pos.Raw.get?.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → Sort u_1) (s : String) (p : String.Pos.Raw)
  (h_1 : (s : String) → (p : String.Pos.Raw) → motive s p),
  (match s, p with
    | s, p => h_1 s p) =
    h_1 s p
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.isometry_mul : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R],
  Isometry ⇑(ContinuousLinearMap.mul 𝕜 R)
-- Mathlib.Algebra.GroupWithZero.Action.Units
IsUnit.smul_eq_zero : ∀ {G : Type u_2} {M : Type u_3} [inst : Monoid G] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction G M] {u : G}
  {x : M}, IsUnit u → (u • x = 0 ↔ x = 0)
-- Mathlib.GroupTheory.IsSubnormal
/-- An additive subgroup `H` is subnormal if there is a subnormal additive subgroup `K`
containing `H` that is subnormal itself and such that `H` is normal in `K`.  -/
AddSubgroup.IsSubnormal.step : ∀ {G : Type u_2} [inst : AddGroup G] (H K : AddSubgroup G),
  H ≤ K → K.IsSubnormal → (H.addSubgroupOf K).Normal → H.IsSubnormal
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsStackFor.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, (F.toDescentData fun f => f.obj.hom).IsEquivalence → F.IsStackFor R
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hasForgetToModuleCat : {k : Type u} →
  {G : Type v} → [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.HasForget₂ (Rep.{w, u, v} k G) (ModuleCat k)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Characterization of parabolic elements: they have the form `a + m` where `a` is scalar and
`m` is nonzero and nilpotent.  -/
Matrix.isParabolic_iff_exists : ∀ {K : Type u_1} [inst : Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2],
  m.IsParabolic ↔ ∃ a n, m = (Matrix.scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The short complex of the `r`th page of the spectral sequence on position `pq'`
identifies to the short complex given by the differentials of the spectral object.
Then, the homology of this short complex can be computed using
`SpectralSequence.dHomologyIso`.
(This only applies in the favourable case when there are `pq` and `pq''` such
that `(c r).Rel pq pq'` and `(c r).Rel pq' pq''` hold.)  -/
CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    [inst_3 : X.HasSpectralSequence data] →
                      (r : ℤ) →
                        (hr : r₀ ≤ r) →
                          (pq pq' pq'' : κ) →
                            (hpq : (c r).Rel pq pq') →
                              (hpq' : (c r).Rel pq' pq'') →
                                (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                  n₂ = data.deg pq' →
                                    (hn₁ :
                                        autoParam (n₀ + 1 = n₁)
                                          CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso._auto_1) →
                                      (hn₂ :
                                          autoParam (n₁ + 1 = n₂)
                                            CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso._auto_3) →
                                        (hn₃ :
                                            autoParam (n₂ + 1 = n₃)
                                              CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso._auto_5) →
                                          (hn₄ :
                                              autoParam (n₃ + 1 = n₄)
                                                CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso._auto_7) →
                                            ((X.spectralSequence data).page r ⋯).sc' pq pq' pq'' ≅
                                              X.dShortComplex (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                                (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                                (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                                (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Order.Defs.Unbundled
/-- `Minimal P x` means that `x` is a minimal element satisfying `P`.  -/
Minimal : {α : Type u_1} → [LE α] → (α → Prop) → α → Prop
-- Mathlib.RingTheory.Filtration
Ideal.iInf_pow_smul_eq_bot_of_isLocalRing : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsNoetherianRing R] [IsLocalRing R] [Module.Finite R M], I ≠ ⊤ → ⨅ i, I ^ i • ⊤ = ⊥
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for finite products in commutative groups with
an ultrametric norm.
 -/
IsUltrametricDist.nnnorm_prod_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  {C : NNReal}, (∀ i ∈ s, ‖f i‖₊ ≤ C) → ‖∏ i ∈ s, f i‖₊ ≤ C
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      ((X : B) → CategoryTheory.ObjectProperty ↑(F.obj X)) → F.ObjectProperty
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_zero : Real.sinh 0 = 0
-- Mathlib.NumberTheory.Pell
/-- The `y` component of a solution to the Pell equation `x^2 - d*y^2 = 1`  -/
Pell.Solution₁.y : {d : ℤ} → Pell.Solution₁ d → ℤ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.lie_e_lie_f_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.e i, ⁅RootPairing.GeckConstruction.f i, RootPairing.GeckConstruction.u j⁆⁆ =
    |b.cartanMatrix i j| • RootPairing.GeckConstruction.u i
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.mem_radical_iff' : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} {m : M},
  m ∈ Q.radical ↔ Q m = 0 ∧ ∀ (n : M), Q (m + n) = Q n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_getKey_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp],
  (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') →
    (∀ (k : α), Std.ExtDTreeMap.Const.get? t₁ k = Std.ExtDTreeMap.Const.get? t₂ k) → t₁ = t₂
-- Lean.Parser.Level
Lean.Parser.Level.num.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.ULift
ULift.down_le : ∀ {α : Type u} [inst : LE α] {a b : ULift.{u_1, u} α}, a.down ≤ b.down ↔ a ≤ b
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `Set α → (E →L[ℝ] F')` to `(α →₁ₛ[μ] E) → F'`.  -/
MeasureTheory.L1.SimpleFunc.setToL1S : {α : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {m : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → (Set α → E →L[ℝ] F) → ↥(α →₁ₛ[μ] E) → F
-- Mathlib.Topology.CompactOpen
ContinuousMap.specializes_coe : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)},
  ⇑f ⤳ ⇑g ↔ f ⤳ g
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.zsmul_mem : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A) {x : A},
  x ∈ S → ∀ (n : ℤ), n • x ∈ S
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.isGroupLikeElem_iff_mem_range_of : ∀ {R : Type u_1} {M : Type u_8} [inst : CommRing R] [IsDomain R] [inst_2 : AddZeroClass M] {x : AddMonoidAlgebra R M},
  IsGroupLikeElem R x ↔ x ∈ Set.range ⇑(AddMonoidAlgebra.of R M)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.pure : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MCasesPat
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.AlterWF.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp} {cut : α → Ordering} {f : Option α → Option α},
  RBTree.RBNode.WF cmp (RBTree.RBNode.alter cut f ↑t) → t.AlterWF cut f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.mk : Lean.MVarId → Lean.Syntax → Lean.Elab.Term.MVarErrorKind → Lean.Elab.Term.MVarErrorInfo
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.ext_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  {f g : BoxIntegral.BoxAdditiveMap ι M I₀}, f = g ↔ ∀ (J : BoxIntegral.Box ι), f J = g J
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.const_sub : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → ∀ (c : F), HasStrictFDerivAt (fun x => c - f x) (-f') x
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₂_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [inst_2 : CategoryTheory.Category.{v_7, u_7} E]
  {E' : Type u_8} [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) {X_1 Y : C₁} (f : X_1 ⟶ Y) (X_2 : C₂),
  (((CategoryTheory.Functor.postcompose₂.obj X).obj F).map f).app X_2 = X.map ((F.map f).app X_2)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.keyAtIdx!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {i : ℕ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdx! i = t₂.keyAtIdx! i
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.mk.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
  (f f_1 : (i : ι) → A.X i ⟶ B.X i) (e_f : f = f_1)
  (comm' :
    ∀ (i j : ι),
      c.Rel i j →
        CategoryTheory.CategoryStruct.comp (f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f j)),
  { f := f, comm' := comm' } = { f := f_1, comm' := ⋯ }
-- Init.Data.Dyadic.Basic
Dyadic.blt.eq_4 : ∀ (a a_1 : ℤ) (a_2 : a % 2 = 1) (b b_1 : ℤ) (b_2 : b % 2 = 1),
  (Dyadic.ofOdd a a_1 a_2).blt (Dyadic.ofOdd b b_1 b_2) =
    match b_1 - a_1 with
    | Int.ofNat l => decide (a <<< l < b)
    | Int.negSucc l => decide (a < b <<< (l + 1))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.conj_eq_snd_of_isCommMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj G],
  CategoryTheory.GrpObj.conj G = CategoryTheory.SemiCartesianMonoidalCategory.snd G G
-- Init.Core
And.comm : ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
-- Init.Grind.Config
/-- If `suggestions` is `true`, `grind` will invoke the currently configured library suggestion engine on the current goal,
and add attempt to use the resulting suggestions as additional parameters to the `grind` tactic.  -/
Lean.Grind.Config.suggestions : Lean.Grind.Config → Bool
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.frob_equivariant : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂]
  (self : WittVector.IsocrystalEquiv p k V V₂) (x : V),
  (WittVector.Isocrystal.frobenius p k) (self.toLinearEquiv x) =
    self.toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.str : (self : TopCat) → TopologicalSpace ↑self
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.symm : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (d : PseudoMetric X R) (x y : X),
  d x y = d y x
-- Lean.Elab.Tactic.Basic
/-- Execute `x` with error recovery disabled  -/
Lean.Elab.Tactic.withoutRecover : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The canonical isomorphism `(free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⊗ Y)`
for two types `X` and `Y`.
(This should not be used directly: it is part of the implementation of the
monoidal structure on the functor `free R`.)  -/
ModuleCat.FreeMonoidal.μIso : (R : Type u) →
  [inst : CommRing R] →
    (X Y : Type u) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj ((ModuleCat.free R).obj X) ((ModuleCat.free R).obj Y) ≅
        (ModuleCat.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Prod.toSigma.eq_1 : ∀ {α : Type u} {β : Type v} (p : α × β), Std.Internal.List.Prod.toSigma p = ⟨p.1, p.2⟩