mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.subgoal.injEq : ∀ (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) (fvarId_1 : Lean.FVarId) (mvarId_1 : Lean.MVarId),
  (Lean.Meta.Match.InjectionAnyResult.subgoal✝ fvarId mvarId =
      Lean.Meta.Match.InjectionAnyResult.subgoal✝ fvarId_1 mvarId_1) =
    (fvarId = fvarId_1 ∧ mvarId = mvarId_1)
-- Mathlib.CategoryTheory.DifferentialObject
/-- The composition of morphisms of differential objects.  -/
CategoryTheory.DifferentialObject.Hom.comp : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            {X Y Z : CategoryTheory.DifferentialObject S C} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toProd : {α : Type u_6} → [inst : LE α] → NonemptyInterval α → α × α
-- Mathlib.Order.UpperLower.Prod
UpperSet.Ici_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (x : α × β),
  UpperSet.Ici x = UpperSet.Ici x.1 ×ˢ UpperSet.Ici x.2
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsMaximal.of_liesOver_isMaximal : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hpm : p.IsMaximal] [P.IsPrime], P.IsMaximal
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.inv_hom_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_subset_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isShortNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3], W.Δ = -W.a₄ ^ 3
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- This is another convenient method to verify that a fork is a weak limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.Fork.IsWeakLimit.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Fork f g) →
          ((s : CategoryTheory.Limits.Fork f g) → { l // CategoryTheory.CategoryStruct.comp l t.ι = s.ι }) →
            CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.CategoryTheory.Adjunction.Whiskering
CategoryTheory.Adjunction.whiskerLeft_counit_app_app : ∀ (C : Type u_1) {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor E C)
  (X_1 : E), ((CategoryTheory.Adjunction.whiskerLeft C adj).counit.app X).app X_1 = X.map (adj.counit.app X_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.badReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasMultiplicativeReduction R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_succ_of_le : ∀ {n : ℕ} (p i : Fin n), i ≤ p → p.succ.succAbove i = i.castSucc
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.leftUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_2 : CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id (⊥_ C)) f)
      (CategoryTheory.Limits.coprod.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.leftUnitor X).hom f
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.dedup.toFinset = m.toFinset
-- Mathlib.RingTheory.KrullDimension.Zero
/-- **Alias** of `Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal`. -/
Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R], minimalPrimes R = {I | I.IsMaximal}
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.map_modifyNth : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (F : Turing.PointedMap Γ Γ') (f : Γ → Γ)
  (f' : Γ' → Γ'),
  (∀ (x : Γ), F.f (f x) = f' (F.f x)) →
    ∀ (n : ℕ) (L : Turing.ListBlank Γ),
      Turing.ListBlank.map F (Turing.ListBlank.modifyNth f n L) =
        Turing.ListBlank.modifyNth f' n (Turing.ListBlank.map F L)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_bot_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), ⊥.extensionProduct P = ⊥
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).get k h' = t.get k ⋯
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult.subgoals.sizeOf_spec : sizeOf Lean.Elab.Tactic.Grind.LiftActionCoreResult.subgoals = 1
-- Std.Do.PostCond
Std.Do.ExceptConds.fst_const : ∀ {ε : Type u} {ps : Std.Do.PostShape} (p : Prop), (Std.Do.ExceptConds.const p).1 = fun _ε => ⌜p⌝
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.id' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.toAddMon
-- Mathlib.Analysis.Normed.Order.Lattice
lipschitzWith_sup_right : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (z : α),
  LipschitzWith 1 fun x => x ⊔ z
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.iso_inv_naturality : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) [h : CategoryTheory.CatCommSq T L R B]
  {x y : C₁} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (B.map (L.map f)) ((CategoryTheory.CatCommSq.iso T L R B).inv.app y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).inv.app x) (R.map (T.map f))
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.absolutelyContinuous_of_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ]
  [h_zero : ∀ (a : α), NeZero (κ a)], (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) → μ.AbsolutelyContinuous ν
-- Mathlib.Algebra.Module.SnakeLemma
SnakeLemma.eq_of_eq : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (f₁ : M₁ →ₗ[R] M₂)
  (f₂ : M₂ →ₗ[R] M₃),
  Function.Exact ⇑f₁ ⇑f₂ →
    ∀ (g₁ : N₁ →ₗ[R] N₂),
      g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
        ∀ (ρ : N₂ → N₁),
          ρ ∘ ⇑g₁ = id →
            ∀ {K₃ : Type u_9} {C₁ : Type u_10} [inst_11 : AddCommGroup K₃] [inst_12 : Module R K₃]
              [inst_13 : AddCommGroup C₁] [inst_14 : Module R C₁] (ι₃ : K₃ →ₗ[R] M₃) (π₁ : N₁ →ₗ[R] C₁),
              Function.Exact ⇑i₁ ⇑π₁ →
                ∀ (x : K₃) (y₁ : M₂),
                  f₂ y₁ = ι₃ x →
                    ∀ (z₁ : N₁), g₁ z₁ = i₂ y₁ → ∀ (y₂ : M₂), f₂ y₂ = ι₃ x → ∀ (z₂ : N₁), g₁ z₂ = i₂ y₂ → π₁ z₁ = π₁ z₂
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `Equiv.cast (congrArg _ h)` as a `MulEquiv`.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
MulEquiv.cast : {ι : Type u_9} → {M : ι → Type u_10} → [inst : (i : ι) → Mul (M i)] → {i j : ι} → i = j → M i ≃* M j
-- Std.Tactic.Do.Syntax
/-- `mexact` is like `exact`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (Q : SPred σs) : Q ⊢ₛ Q := by
  mstart
  mintro HQ
  mexact HQ
```
 -/
Lean.Parser.Tactic.mexact : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffAddEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddMonoidAlgebra.coeffAddEquiv = AddMonoidAlgebra.coeffEquiv.addEquiv
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.anyM : {α : Type u_1} →
  [inst : BEq α] →
    {m : Type → Type u_2} →
      [Monad m] → (α → m Bool) → (s : Aesop.UnorderedArraySet α) → optParam ℕ 0 → optParam ℕ s.size → m Bool
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.isClosed_aestronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [CompleteSpace F],
  m ≤ m0 → IsClosed {f | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Matrix.trace_eq_sum_roots_charpoly : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {K : Type u_3} [inst_2 : Field K] (A : Matrix n n K)
  [IsAlgClosed K], A.trace = A.charpoly.roots.sum
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a - ⊤ = ⊤
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_shiftLeft_cancel : ∀ {a : ℤ} {b : ℕ}, 2 ^ b ∣ a → a >>> b <<< b = a
-- Aesop.Frontend.Saturate
Aesop.Frontend.saturate? : Lean.ParserDescr
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIsoAt.mk : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} {f : K ⟶ L}
  {i : ι} [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f) → QuasiIsoAt f i
-- Mathlib.Topology.Instances.Rat
Rat.instIsTopologicalRing : IsTopologicalRing ℚ
-- Init.Data.UInt.Lemmas
UInt64.eq_iff_toBitVec_eq : ∀ {a b : UInt64}, a = b ↔ a.toBitVec = b.toBitVec
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.custom : IO.Ref Lean.Elab.Term.State → Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.Simp.DischargeWrapper
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_apply_ne' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) {i j : n},
  j ≠ i → Matrix.diagonal d i j = 0
-- Mathlib.Data.Nat.Fib.Basic
/-- **Alias** of `Nat.fastFib_eq`. -/
Nat.fast_fib_eq : ∀ (n : ℕ), n.fastFib = Nat.fib n
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le : ∀ {α : 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 α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  0 ≤ C → ‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ C
-- Std.Http.Data.Chunk
/-- Adds an extension to a chunk.
 -/
Std.Http.Chunk.insertExtension : Std.Http.Chunk → Std.Http.Chunk.ExtensionName → Std.Http.Chunk.ExtensionValue → Std.Http.Chunk
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.cast_apply : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M i),
  (AddEquiv.cast h) a = cast ⋯ a
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multispan used to define the coend
of `F`.  -/
CategoryTheory.Limits.multispanIndexCoend : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) →
          CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.multispanShapeCoend J) C
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.IsComplex.mult_eq_two : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, w.IsComplex → w.mult = 2
-- LeanSearchClient.Syntax
LeanSearchClient.leanSearchServer : LeanSearchClient.SearchServer
-- Mathlib.Computability.RecursiveIn
/-- A partial function `f` is partial recursive if and only if it is recursive in
every partial function `g`.  -/
partrec_iff_forall_recursiveIn_singleton : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ},
  Partrec f ↔ ∀ (g : ℕ →. ℕ), RecursiveIn {g} f
-- Init.PropLemmas
Decidable.not_iff : ∀ {b a : Prop} [Decidable b], ¬(a ↔ b) ↔ (¬a ↔ b)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le`. -/
CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_of_hasCardinalLT_of_le : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) {κ' : Cardinal.{u}}
  [inst_1 : Fact κ'.IsRegular], HasCardinalLT (↑J.obj) κ' → κ ≤ κ' → CategoryTheory.IsCardinalPresentable J κ'
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_one : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Matrix.ProjGenLinGroup.mk 1 = 1
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent additive group is the smallest natural `n`
such that the `n`-th term of the upper central series is `G`. If `G` is not nilpotent then the
nilpotency class takes the junk value 0.  -/
AddGroup.nilpotencyClass : (G : Type u_1) → [AddGroup G] → ℕ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.shift_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a : ℤ), ↑(γ.shift a) = (↑γ).shift a
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M' → M}
  {s : Set M'}, ContMDiffOn I' (I.transContinuousLinearEquiv e) n f s ↔ ContMDiffOn I' I n f s
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking that declarations don't have unused term mode have statements.  -/
Batteries.Tactic.Lint.unusedHavesSuffices : Batteries.Tactic.Lint.Linter
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_comp_neg : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {β : Type u_4} [inst_2 : InvolutiveNeg β]
  (f : β → α), ∑' (d : β), f (-d) = ∑' (d : β), f d
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A category is called preadditive if `P ⟶ Q` is an abelian group such that composition is
linear in both variables.  -/
CategoryTheory.Preadditive.add_comp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Preadditive C] (P Q R : C)
  (f f' : P ⟶ Q) (g : Q ⟶ R),
  CategoryTheory.CategoryStruct.comp (f + f') g =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- An injective morphism of vector spaces induces an injective morphism of exterior algebras.  -/
ExteriorAlgebra.map_injective_field : ∀ {K : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Field K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : AddCommGroup F] [inst_4 : Module K F] {f : E →ₗ[K] F},
  f.ker = ⊥ → Function.Injective ⇑(ExteriorAlgebra.map f)
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.unitsSMul.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : Module.Basis ι R M) (w : ι → Rˣ), v.unitsSMul w = Module.Basis.mk ⋯ ⋯
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_pos : ∀ {n : ℕ}, 0 < n.greatestFib ↔ 0 < n
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.instFaithfulSMul_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (i : ι), FaithfulSMul (G i) (Monoid.PushoutI.NormalWord d)
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (S : Set α), UpperSet.Ici (sSup S) = ⨆ a ∈ S, UpperSet.Ici a
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instInhabitedFunPropDecls.default : Mathlib.Meta.FunProp.FunPropDecls
-- Mathlib.Analysis.Normed.Module.Bases
/-- Data for constructing a Schauder basis from a sequence of finite-rank projections.

Given a sequence of continuous linear maps `P n : X →L[𝕜] X` satisfying:
* `P 0 = 0` and `finrank(range(P n)) = n`,
* `P n ∘ P m = P (min n m)` (the projections are nested and commute),
* `P n x → x` for every `x` (pointwise convergence to the identity),

the differences `succSub P n = P (n+1) - P n` are rank-one operators
(see `finrank_range_succSub_eq_one`). Choosing a nonzero vector `e n` in the range of each
`succSub P n` yields a Schauder basis for `X`.

Use `RankOneDecomposition.basis` to construct the `SchauderBasis` from this data.  -/
SchauderBasis.RankOneDecomposition : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] → (X : Type u_2) → [inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → Type u_2
-- Mathlib.Logic.Equiv.Set
Equiv.preimage_symm_preimage : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α), ⇑e ⁻¹' ⇑e.symm ⁻¹' s = s
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMaxOn.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsMaxOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDeriv ℝ f a b = 0
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_concat_of_endsWithVar : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op]
  (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.endsWithVar_k x = true →
    Lean.Grind.AC.Seq.denote ctx (s.concat_k (Lean.Grind.AC.Seq.var x)) = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R)
  {T : CategoryTheory.Functor Eᵒᵖ RingCat} {G : CategoryTheory.Functor D E} (ψ : R ⟶ G.op.comp T)
  {T' : CategoryTheory.Functor E'ᵒᵖ RingCat} {G' : CategoryTheory.Functor E E'} (ψ' : T ⟶ G'.op.comp T'),
  (PresheafOfModules.pushforward ψ').isoWhiskerLeft (PresheafOfModules.pushforwardComp φ ψ) ≪≫
      PresheafOfModules.pushforwardComp (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ)) ψ' =
    ((PresheafOfModules.pushforward ψ').associator (PresheafOfModules.pushforward ψ)
          (PresheafOfModules.pushforward φ)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pushforwardComp ψ ψ')
          (PresheafOfModules.pushforward φ) ≪≫
        PresheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.comp ψ (G.op.whiskerLeft ψ'))
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The short root `α + β`.  -/
RootPairing.EmbeddedG2.shortAddLongRoot : {ι : 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) → [P.EmbeddedG2] → M
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
MvPolynomial.comap_C_surjective : ∀ {R : Type u_2} [inst : CommRing R] {σ : Type u_1}, Function.Surjective (PrimeSpectrum.comap MvPolynomial.C)
-- Mathlib.Algebra.Category.ModuleCat.Projective
/-- Modules that have a basis are projective.  -/
ModuleCat.projective_of_free : ∀ {R : Type u} [inst : Ring R] {M : ModuleCat R} {ι : Type w} (b : Module.Basis ι R ↑M), CategoryTheory.Projective M
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_filter : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [inst_3 : DecidablePred p] (f : Π₀ (i : ι), β i),
  (DFinsupp.filter p f).support = {x ∈ f.support | p x}
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_lt_iff_of_pos : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z⁻¹ < y ↔ x < y ^ z)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_neg`. -/
ModularForm.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Init.Data.Order.Classes
/-- This typeclass states that `min a b = if a ≤ b then a else b` (for any `DecidableLE α` instance).
 -/
Std.LawfulOrderLeftLeaningMin : (α : Type u) → [Min α] → [LE α] → Prop
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.unicode : Lean.Option Bool
-- Mathlib.LinearAlgebra.Projection
/-- An idempotent operator `f` commutes with a unit operator `T` if and only if
`T (range f) = range f` and `T (ker f) = ker f`.  -/
LinearMap.IsIdempotentElem.commute_iff_of_isUnit : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsUnit T → IsIdempotentElem f → (Commute f T ↔ Submodule.map T f.range = f.range ∧ Submodule.map T f.ker = f.ker)
-- Mathlib.Computability.ContextFreeGrammar
/-- Grammar for a reversed language.  -/
ContextFreeGrammar.reverse : {T : Type u_1} → ContextFreeGrammar T → ContextFreeGrammar T
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iio_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iio a)), Subtype.val '' Set.Ici b = Set.Ico (↑b) a