mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapAugmentedCechNerve_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g),
  (CategoryTheory.Arrow.mapAugmentedCechNerve F).left = CategoryTheory.Arrow.mapCechNerve F
-- Mathlib.Data.Finset.Card
/-- Given a surjective map `f` from a finite set `s` to another finite set `t`, if `s` is no larger
than `t`, then `f` is injective when restricted to `s`.
See `Finset.inj_on_of_surj_on_of_card_le` for the version where `f` is a dependent function.
 -/
Finset.injOn_of_surjOn_of_card_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β),
  Set.MapsTo f ↑s ↑t → Set.SurjOn f ↑s ↑t → s.card ≤ t.card → Set.InjOn f ↑s
-- Init.Data.Int.Gcd
Int.natAbs_le_lcm_left : ∀ {b : ℤ} (a : ℤ), b ≠ 0 → a.natAbs ≤ a.lcm b
-- Mathlib.RingTheory.RingInvo
RingInvo.instEquivLikeMulOpposite : {R : Type u_2} → [inst : Semiring R] → EquivLike (RingInvo R) R Rᵐᵒᵖ
-- Init.Data.List.Lemmas
List.dropLast_cons_self_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (a :: List.replicate n a).dropLast = List.replicate n a
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_int_mod : ∀ (s : Multiset ℤ) (n : ℤ), s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.nth.eq_3 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (n : ℕ), T.nth (Int.negSucc n) = T.left.nth n
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- Note that the name is to match `CanonicallyOrderedAdd.mul_pos`.  -/
CanonicallyOrderedAdd.prod_pos : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] {f : ι → R}
  {s : Finset ι} [NoZeroDivisors R] [Nontrivial R], 0 < ∏ i ∈ s, f i ↔ ∀ i ∈ s, 0 < f i
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- `n.succ`-pretransitivity implies `n`-preprimitivity.  -/
AddAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succ : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {n : ℕ},
  ↑n.succ ≤ ENat.card α → ∀ [AddAction.IsMultiplyPretransitive M α n.succ], AddAction.IsMultiplyPreprimitive M α n
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_monomial_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (a : R),
  a ≠ 0 → ((MvPolynomial.monomial s) a).degrees = Finsupp.toMultiset s
-- Init.Data.Array.Lemmas
Array.mapM_eq_mapM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α},
  Array.mapM f xs = List.toArray <$> List.mapM f xs.toList
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.smulCommClass_symm_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Mul M]
  [SMulCommClass S R S], SMulCommClass (MonoidAlgebra S M) R (MonoidAlgebra S M)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.startsWith_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → s.startsWith pat = t.startsWith pat
-- Mathlib.Order.RelIso.Basic
/-- An equivalence `f : α ≃ β` induces a relation isomorphism from an `α`-relation `r` to
`Relation.Map r f f`.  -/
RelIso.toMap : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (f : α ≃ β) → r ≃r Relation.Map r ⇑f ⇑f
-- Lean.Data.Json.Basic
Lean.Json.getNum? : Lean.Json → Except String Lean.JsonNumber
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.range_cos : Set.range Real.cos = Set.Icc (-1) 1
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.le_comap_of_ramificationIdx'_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, p.ramificationIdx' P ≠ 0 → p ≤ Ideal.comap (algebraMap R S) P
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Data.Matrix.Basis
Matrix.liftLinear_singleLinearMap : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : Module R α] [inst_8 : Module S α] [inst_9 : SMulCommClass R S α],
  (Matrix.liftLinear S) (Matrix.singleLinearMap R) = LinearMap.id
-- Init.Data.BitVec.Lemmas
BitVec.umod.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.umod y = (x.toNat % y.toNat)#'⋯
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_prop_eq_some_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos pos' : s.Pos},
  pos.find? p = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), p (pos'.get h)) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), ¬p (pos''.get ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits.0.CategoryTheory.WithTerminal.map.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a a_1 : C)
  (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1)
  (h_1 :
    (a a_2 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_2) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_2) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_2, f => h_1 a a_2 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 a a_1 f
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The precomposition map `RightHomotopyClass Y Z → (X ⟶ Y) → RightHomotopyClass X Z`.  -/
HomotopicalAlgebra.RightHomotopyClass.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.RightHomotopyClass Y Z → (X ⟶ Y) → HomotopicalAlgebra.RightHomotopyClass X Z
-- Mathlib.Analysis.Quaternion
Quaternion.tsum_coe : ∀ {α : Type u_1} {L : SummationFilter α} (f : α → ℝ), ∑'[L] (a : α), ↑(f a) = ↑(∑'[L] (a : α), f a)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_sum_filter : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq α] (f : β → α)
  (s : Finset β) (g : β → M), ∑ᶠ (x : α), ∑ y ∈ s with f y = x, g y = ∑ k ∈ s, g k
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.setLike : {R : Type v} → [inst : NonAssocSemiring R] → [inst_1 : Star R] → SetLike (StarSubsemiring R) R
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.minD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_mul : ∀ (z w : Complex.UnitClosedDisc), ↑(z * w) = ↑z * ↑w
-- Mathlib.Algebra.Algebra.Pi
/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as an `AlgEquiv`.
 -/
AlgEquiv.piCongrLeft' : (R : Type u_3) →
  {ι : Type u_4} →
    (A₁ : ι → Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A₁ i)] →
          [inst_2 : (i : ι) → Algebra R (A₁ i)] →
            {ι' : Type u_8} → (e : ι ≃ ι') → ((i : ι) → A₁ i) ≃ₐ[R] (i : ι') → A₁ (e.symm i)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.offset_lt_rawEndPos_iff : ∀ {s : String.Slice} {p : s.Pos}, p.offset < s.rawEndPos ↔ p ≠ s.endPos
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.mapM f it) =
    Std.IterM.foldM
      (fun d b => do
        let c ← f b
        pure (g d c))
      init it
-- Mathlib.MeasureTheory.Measure.Stieltjes
Ioc_sdiff_botSet : ∀ {R : Type u_1} [inst : LinearOrder R] (a b : R), Set.Ioc a b \ botSet = Set.Ioc a b
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ},
  0 < n → (addOrderOf x = n ↔ n • x = 0 ∧ ∀ m < n, 0 < m → m • x ≠ 0)
-- Mathlib.Algebra.Star.Module
selfAdjointPart_comp_subtype_selfAdjoint : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2], selfAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = LinearMap.id
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)) {s : Set (((i : ι) → Em i) × G)}
  {x : ((i : ι) → Em i) × G}, AnalyticWithinAt 𝕜 (fun p => (f p.1) p.2) s x
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indep_comap_pi_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [inst_4 : Fintype S]
  [MeasureTheory.IsProbabilityMeasure P],
  m ≤ mΩ →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
              ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap (fun ω s => X s ω) MeasurableSpace.pi) P
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.ofCocone_ℐ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [inst_2 : CategoryTheory.IsFiltered I] {F : CategoryTheory.Functor I C}
  (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).ℐ = inst_1
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- A trivial fiber bundle with fiber `F` over a base `B` is a space `Z`
projecting on `B` for which there exists a homeomorphism to `B × F` that sends `proj`
to `Prod.fst`.  -/
IsHomeomorphicTrivialFiberBundle : {B : Type u_1} →
  (F : Type u_2) → {Z : Type u_3} → [TopologicalSpace B] → [TopologicalSpace F] → [TopologicalSpace Z] → (Z → B) → Prop
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `H` is commutative and `G →* H` is injective, then `G` is commutative.  -/
MonoidHom.commGroupOfInjective : {G : Type u_5} →
  {H : Type u_6} → [inst : Group G] → [inst_1 : CommGroup H] → (f : G →* H) → Function.Injective ⇑f → CommGroup G
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.mgf X μ 0 = 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.update.eq_1 : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M),
  f.update a b = { coeff := f.coeff.update a b }
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The functor taking a monoid to its subgroup of units.  -/
CommMonCat.units : CategoryTheory.Functor CommMonCat CommGrpCat
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_sub_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g₁ g₂ : Π₀ (a : α), N a), (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_one : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M), ↑1 = 1
-- Mathlib.Topology.Sheaves.Abelian
/-- A sheaf is zero if and only if its stalks are all zero.  -/
TopCat.Sheaf.isZero_iff_stalkFunctor_obj_isZero : ∀ {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  [CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u}
  [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Abelian C] {X : TopCat}
  (F : TopCat.Sheaf C X),
  CategoryTheory.Limits.IsZero F ↔
    ∀ (x : ↑X), CategoryTheory.Limits.IsZero (((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x)).obj F)
-- Mathlib.Data.PNat.Basic
instMulPNat : Mul ℕ+
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The `Subring` generated by a set.  -/
Subring.closure : {R : Type u} → [inst : NonAssocRing R] → Set R → Subring R
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_sdiff_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  (s.biUnion fun a => Finset.image (fun x => a \ x) t) = s.diffs t
-- Init.Data.Int.LemmasAux
Int.min_self_assoc : ∀ {m n : ℤ}, min m (min m n) = min m n
-- Std.Time.Format.Modifier
Std.Time.Modifier.O.injEq : ∀ (presentation presentation_1 : Std.Time.OffsetO),
  (Std.Time.Modifier.O presentation = Std.Time.Modifier.O presentation_1) = (presentation = presentation_1)
-- Init.Data.List.Sublist
List.isPrefixOf_cons₂_self : ∀ {α : Type u_1} [inst : BEq α] {as bs : List α} [LawfulBEq α] {a : α},
  (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs
-- Mathlib.Order.Heyting.Regular
Heyting.isRegular_compl : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : α), Heyting.IsRegular aᶜ
-- Lean.LocalContext
Lean.LocalDecl.isAuxDecl : Lean.LocalDecl → Bool
-- Init.Data.String.Basic
String.Pos.Raw.get'_eq : ∀ (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true),
  String.Pos.Raw.get' s p h = String.Pos.Raw.get s p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_neg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  [ContinuousMap.UniqueHom R A],
  autoParam (ContinuousOn f ((fun x => -x) '' spectrum R a)) cfc_comp_neg._auto_1 →
    autoParam (p a) cfc_comp_neg._auto_3 → cfc (fun x => f (-x)) a = cfc f (-a)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Associativity of the `L^p` product as a linear isometric equivalence.  -/
LinearIsometryEquiv.withLpProdAssoc : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        (γ : Type u_4) →
          [hp : Fact (1 ≤ p)] →
            [inst : Semiring 𝕜] →
              [inst_1 : SeminormedAddCommGroup α] →
                [inst_2 : Module 𝕜 α] →
                  [inst_3 : SeminormedAddCommGroup β] →
                    [inst_4 : Module 𝕜 β] →
                      [inst_5 : SeminormedAddCommGroup γ] →
                        [inst_6 : Module 𝕜 γ] → WithLp p (WithLp p (α × β) × γ) ≃ₗᵢ[𝕜] WithLp p (α × WithLp p (β × γ))
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.instIsTorsionFree : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [Module.IsTorsionFree R S], Module.IsTorsionFree R (MonoidAlgebra S M)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.eq_def : ∀ (n : ℕ) (x : Fin (n + 3)),
  SimpleGraph.cycleGraph.cycleCons✝ n x =
    match x with
    | ⟨0, h⟩ => SimpleGraph.Walk.nil
    | ⟨m.succ, h⟩ =>
      have hadj := ⋯;
      SimpleGraph.Walk.cons hadj (SimpleGraph.cycleGraph.cycleCons✝ n ⟨m, ⋯⟩)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rcc_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toArray.getD i fallback = m + ↑i
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Exactness of `J`-shaped colimits stated as `colim : (J ⥤ C) ⥤ C` preserving finite limits.  -/
CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits : ∀ {J : Type u'} {inst : CategoryTheory.Category.{v', u'} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C} [self : CategoryTheory.HasExactColimitsOfShape J C],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
-- Mathlib.Analysis.Calculus.Deriv.Comp
derivWithin.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'}
  {g₁ : 𝕜' → F} {y : 𝕜'},
  DifferentiableWithinAt 𝕜' g₁ t' y →
    DifferentiableWithinAt 𝕜 h s x →
      Set.MapsTo h s t' → y = h x → derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.chebyshevTsequence.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NeZero 2],
  Polynomial.Chebyshev.chebyshevTsequence R = Polynomial.Chebyshev.chebyshevTsequence R
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_iff_left : ∀ {a b n : ℕ}, n ≠ 0 → (a ^ n < b ^ n ↔ a < b)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two coforks of the form `ofπ` are isomorphic whenever their `π`'s are equal.  -/
CategoryTheory.Limits.CoforkOfπ.ext : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {P : C} →
          {π π' : Y ⟶ P} →
            (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) →
              (w' : CategoryTheory.CategoryStruct.comp f π' = CategoryTheory.CategoryStruct.comp g π') →
                π = π' → (CategoryTheory.Limits.Cofork.ofπ π w ≅ CategoryTheory.Limits.Cofork.ofπ π' w')
-- Init.Data.Array.Basic
Array.size_push : ∀ {α : Type u} {xs : Array α} (v : α), (xs.push v).size = xs.size + 1
-- Aesop.Rule
Aesop.instInhabitedSafety : Inhabited Aesop.Safety
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- This definition allows to endow `α × β` with the Lp distance with the uniformity and bornology
being defeq to the product ones. It is useful to endow a type synonym of `a × β` with the
Lp distance.  -/
WithLp.pseudoMetricSpaceToProd : (p : ENNReal) →
  [hp : Fact (1 ≤ p)] →
    (α : Type u_4) → (β : Type u_5) → [PseudoMetricSpace α] → [PseudoMetricSpace β] → PseudoMetricSpace (α × β)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `MDifferentiableAt` and `DifferentiableAt` coincide  -/
mdifferentiableAt_iff_differentiableAt : ∀ {𝕜 : 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 : E → E'}
  {x : E}, MDiffAt f x ↔ DifferentiableAt 𝕜 f x
-- Init.Data.Vector.Lemmas
Vector.forall_mem_replicate : ∀ {α : Type u_1} {p : α → Prop} {a : α} {n : ℕ}, (∀ b ∈ Vector.replicate n a, p b) ↔ n = 0 ∨ p a
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_nat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ), f (x + ↑n) = f x + n • b
-- Mathlib.Order.Closure
ClosureOperator.mk'_isClosed : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x)
  (hf₃ : ∀ (x : α), f (f x) ≤ f x) (x : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
IsPrimitiveRoot.autToPow.congr_simp : ∀ (R : Type u_4) {S : Type u_5} [inst : CommRing S] [inst_1 : IsDomain S] {μ μ_1 : S} (e_μ : μ = μ_1) {n : ℕ}
  (hμ : IsPrimitiveRoot μ n) [inst_2 : CommRing R] [inst_3 : Algebra R S] [inst_4 : NeZero n],
  IsPrimitiveRoot.autToPow R hμ = IsPrimitiveRoot.autToPow R ⋯
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_symm : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂),
  (LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMap₂ b₁ b₂
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.union : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.WF → t₂.WF → (t₁ ∪ t₂).WF
-- Mathlib.Algebra.Group.Int.Even
Int.even_pow : ∀ {m : ℤ} {n : ℕ}, Even (m ^ n) ↔ Even m ∧ n ≠ 0
-- Mathlib.Order.Shrink
orderIsoShrink_symm_apply : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] (a : Shrink.{u, u_1} α),
  (orderIsoShrink α).symm a = (equivShrink α).symm a