mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.limit.w_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (f : j ⟶ j')
  {F_1 : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory C F_1] (x : carrier (CategoryTheory.Limits.limit F)),
  (CategoryTheory.ConcreteCategory.hom (F.map f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j')) x
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algebraMap_monomial : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (n : ℕ) (a : K),
  (algebraMap (Polynomial K) (RatFunc K)) ((Polynomial.monomial n) a) = RatFunc.C a * RatFunc.X ^ n
-- Mathlib.Data.Nat.Factors
/-- For positive `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b`  -/
Nat.perm_primeFactorsList_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable` and
`LawfulUpwardEnumerableLT` instances.
 -/
Std.Roc.isEmpty : {α : Type u} → [inst : LT α] → [DecidableLT α] → [Std.PRange.UpwardEnumerable α] → Std.Roc α → Bool
-- Mathlib.Data.PNat.Defs
PNat.instInhabited : Inhabited ℕ+
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.natTransΓRes_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (U : Cᵒᵖ) (F : CategoryTheory.Sheaf J A),
  (CategoryTheory.Sheaf.natTransΓRes J A U).app F = F.ΓRes U
-- Mathlib.MeasureTheory.Function.Floor
Nat.measurable_ceil : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [OpensMeasurableSpace R], Measurable Nat.ceil
-- Mathlib.Analysis.SpecificLimits.Fibonacci
/-- The limit of `fib n / fib (n + 1)` as `n → ∞` is the negative conjugate of the golden ratio.  -/
tendsto_fib_div_fib_succ_atTop : Filter.Tendsto (fun n => ↑(Nat.fib n) / ↑(Nat.fib (n + 1))) Filter.atTop (nhds (-Real.goldenConj))
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.of_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsCancelAdd M], Function.Injective ⇑Algebra.GrothendieckAddGroup.of
-- Mathlib.Topology.Constructions
Pi.induced_precomp : ∀ {Y : Type v} {ι : Type u_5} [inst : TopologicalSpace Y] {ι' : Type u_9} (φ : ι' → ι),
  TopologicalSpace.induced (fun x => x ∘ φ) Pi.topologicalSpace =
    ⨅ i', TopologicalSpace.induced (Function.eval (φ i')) inst
-- Mathlib.Order.Preorder.Chain
IsChain.exists3 : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r],
  IsChain r s → ∀ [IsTrans α r] {a b c : α}, a ∈ s → b ∈ s → c ∈ s → ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.coe_inv : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  (A : ↥(Matrix.symplecticGroup l R)), ↑A⁻¹ = -Matrix.J l R * (↑A).transpose * Matrix.J l R
-- Mathlib.Topology.Compactness.Compact
/-- If `s` and `t` are compact sets, then the set neighborhoods filter of `s ×ˢ t`
is the product of set neighborhoods filters for `s` and `t`.

For general sets, only the `≤` inequality holds, see `nhdsSet_prod_le`.  -/
IsCompact.nhdsSet_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsCompact s → IsCompact t → nhdsSet (s ×ˢ t) = nhdsSet s ×ˢ nhdsSet t
-- Mathlib.Data.Int.Init
Int.pred_neg_pred : ∀ (a : ℤ), (-a.pred).pred = -a
-- Mathlib.Analysis.Seminorm
Seminorm.continuous' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.closedBall 0 r ∈ nhds 0 → Continuous ⇑p
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.infinite : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] {x : A},
  Transcendental R x → Infinite A
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOrigin x k = 0` for `n ≤ k`.  -/
FormalMultilinearSeries.changeOrigin_finite_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ {k : ℕ}, n ≤ k → p.changeOrigin x k = 0
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedLocalTimeType.default : Std.Time.TimeZone.TZif.LocalTimeType
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- The value of `χ₈ n`, for `n : ℤ`, depends only on `n % 8`.  -/
ZMod.χ₈_int_mod_eight : ∀ (n : ℤ), ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
-- Mathlib.LinearAlgebra.FreeModule.PID
dvd_generator_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [inst_1 : Submodule.IsPrincipal I] {x : R},
  x ∈ I → (x ∣ Submodule.IsPrincipal.generator I ↔ I = Ideal.span {x})
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.mem_prod : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {p : Submodule R M} {q : Submodule R M'} {x : M × M'},
  x ∈ p.prod q ↔ x.1 ∈ p ∧ x.2 ∈ q
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (y : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match none, some y with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_3 y
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The restriction of a module along an open immersion.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctorAdjCounitIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.restrictFunctor f) ≅
        CategoryTheory.Functor.id X.Modules
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The composition functor is also the composition on commutative group objects.  -/
CategoryTheory.Functor.mapCommGrpCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {E : Type u₃} →
                  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] →
                    [inst_7 : CategoryTheory.CartesianMonoidalCategory E] →
                      [inst_8 : CategoryTheory.BraidedCategory E] →
                        {F : CategoryTheory.Functor C D} →
                          [inst_9 : F.Braided] →
                            {G : CategoryTheory.Functor D E} →
                              [inst_10 : G.Braided] → (F.comp G).mapCommGrp ≅ F.mapCommGrp.comp G.mapCommGrp
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.φ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.kernelCokernelCompSequence.φ f g =
    CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl)
      (CategoryTheory.Limits.biprod.lift (-CategoryTheory.CategoryStruct.id Y) g)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.modifyKey_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((_ : α) × β)} {k : α} {f : β → β},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.Const.modifyKey k f l).Perm (Std.Internal.List.Const.modifyKey k f l')
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBot_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β), (f.comp g).withBot = f.withBot.comp g.withBot
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_bot : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M),
  a • ⊥ = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isContained_top_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V}, G.IsContained (SimpleGraph.completeGraph W) ↔ Nonempty (V ↪ W)
-- Mathlib.Data.Finsupp.Weight
/-- If `M` is a `CanonicallyOrderedAddCommMonoid`, then `weight f` is zero iff `f = 0`.  -/
Finsupp.weight_eq_zero_iff_eq_zero : ∀ {σ : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M]
  [CanonicallyOrderedAdd M] (w : σ → M) [Finsupp.NonTorsionWeight ℕ w] {f : σ →₀ ℕ}, (Finsupp.weight w) f = 0 ↔ f = 0
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
_private.Lean.Meta.Tactic.Grind.EMatchTheoremParam.0.Lean.Meta.Grind.toGrindParam : Lean.TSyntax [`Lean.Parser.Tactic.grindLemma, `Lean.Parser.Tactic.grindLemmaMin] →
  Lean.TSyntax `Lean.Parser.Tactic.grindParam
-- Mathlib.FieldTheory.SeparableClosure
/-- The separable closure of `F` in `E` is algebraic over `F`.  -/
separableClosure.isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Algebra.IsAlgebraic F ↥(separableClosure F E)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.btrueExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.mk : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} →
          {u : β → α} →
            (choice : (x : α) → u (l x) ≤ x → β) →
              GaloisConnection l u →
                (∀ (x : β), x ≤ l (u x)) → (∀ (a : α) (h : u (l a) ≤ a), choice a h = l a) → GaloisInsertion l u
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₂ * log (n₁ + n₂))`. Merges the maps `t₁` and `t₂`.
If equal keys exist in both, the key from `t₂` is preferred.
 -/
RBTree.RBSet.union : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → RBTree.RBSet α cmp → RBTree.RBSet α cmp
-- Mathlib.Data.Fintype.Inv
Fintype.rightInverse_bijInv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (f_bij : Function.Bijective f),
  Function.RightInverse (Fintype.bijInv f_bij) f
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr.loop.match_1.eq_2 : ∀ {α : Sort u_2} (n : ℕ) (motive : (x : ℕ) → x ≤ n → α → Sort u_1) (i : ℕ) (h : i + 1 ≤ n) (x : α)
  (h_1 : (x : 0 ≤ n) → (x_1 : α) → motive 0 x x_1) (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive i.succ h x),
  (match i.succ, h, x with
    | 0, x, x_1 => h_1 x x_1
    | i.succ, h, x => h_2 i h x) =
    h_2 i h x
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_assoc_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₄]
  [inst_8 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_9 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₄]
  [inst_10 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₃ F₄] {Z : V}
  (h : CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₃ F₄)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₃ F₄))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₃ F₄) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₂ F₃ F₄))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₄) h)
-- Mathlib.Order.WellFounded
WellFounded.min.eq_1 : ∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty), H.min s h = Classical.choose ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_ne_top_of_nonneg' : ∀ {y : ℝ} {x : ENNReal}, 0 < x → x ≠ ⊤ → x ^ y ≠ ⊤
-- Mathlib.Data.Set.NAry
Set.image2_left_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : Set α} {t : Set β}
  {u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) →
    Set.image2 f s (Set.image2 g t u) = Set.image2 g' t (Set.image2 f' s u)
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.kDecidableEq : (self : Turing.FinTM2) → DecidableEq self.K
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.top_lowerCentralSeries_pi_of_finite : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] [Finite η] (n : ℕ),
  ⊤.lowerCentralSeries n = AddSubgroup.pi Set.univ fun i => ⊤.lowerCentralSeries n
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.integrable_bernoulliMeasure : ∀ {X : Type u_1} [inst : MeasurableSpace X] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [MeasurableSingletonClass X]
  (x y : X) (p : ↑unitInterval) (f : X → E), MeasureTheory.Integrable f (ProbabilityTheory.bernoulliMeasure x y p)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeries_ext_subring : ∀ (K : Type u_2) [inst : Field K],
  Subring.map (LaurentSeries.LaurentSeriesRingEquiv K).toRingHom (LaurentSeries.powerSeries_as_subring K) =
    (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)).toSubring
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_u_bot : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderBot α] {u : α → β} {l : β → α},
  GaloisConnection l u → l (u ⊥) = ⊥
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instReflectsIsomorphismsPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.forget R).ReflectsIsomorphisms
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.noConfusionType : Sort v✝ → Lean.Elab.WF.GuessLex.GuessLexRel → Lean.Elab.WF.GuessLex.GuessLexRel → Sort v✝
-- Mathlib.Data.Num.Lemmas
PosNum.succ.eq_2 : ∀ (n : PosNum), n.bit1.succ = n.succ.bit0
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_univ : ∀ {α : Type u} [h : Infinite α], Set.univ.Infinite
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.denseRange : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsDominant f], DenseRange ⇑f
-- Mathlib.Analysis.Normed.Group.Basic
edist_mulIndicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedGroup E] (s t : Set α) (f : α → E) (x : α),
  edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(symmDiff s t).mulIndicator f x‖₊
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.comp_lcm : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ} {g : α → α},
  Function.Commute f g →
    Function.IsPeriodicPt f m x → Function.IsPeriodicPt g n x → Function.IsPeriodicPt (f ∘ g) (m.lcm n) x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, a ∈ m.erase k → a ∈ m
-- Std.Time.Duration
/-- Creates a new `Duration` out of `Millisecond.Offset`.
 -/
Std.Time.Duration.ofMillisecond : Std.Time.Millisecond.Offset → Std.Time.Duration
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_mono_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {h : Y ⟶ Y},
  CategoryTheory.CategoryStruct.comp h f = f ↔ h = CategoryTheory.CategoryStruct.id Y
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.tensorHom_def : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom Y₁) (g : X₂.Hom Y₂),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Init.Data.Array.Zip
Array.zipWith_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs ys : Array γ} {f : α → β → γ} {as : Array α} {bs : Array β},
  Array.zipWith f as bs = xs ++ ys ↔
    ∃ as₁ as₂ bs₁ bs₂,
      as₁.size = bs₁.size ∧
        as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = Array.zipWith f as₁ bs₁ ∧ ys = Array.zipWith f as₂ bs₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Y_eq_iff : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, P 2 ≠ 0 → Q 2 ≠ 0 → (P 1 * Q 2 = Q 1 * P 2 ↔ P 1 / P 2 = Q 1 / Q 2)
-- Mathlib.CategoryTheory.Limits.Filtered
/-- Class for having cofiltered limits.  -/
CategoryTheory.Limits.HasCofilteredLimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, 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, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Data.Nat.Set
Nat.range_succ : Set.range Nat.succ = {i | 0 < i}
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_counitIso_inv_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core D), (E.core.counitIso.inv.app X).iso.hom = E.counitIso.inv.app X.of
-- Mathlib.Data.Seq.Defs
Stream'.Seq.coinduction2 : ∀ {α : Type u} {β : Type v} (s : Stream'.Seq α) (f g : Stream'.Seq α → Stream'.Seq β),
  (∀ (s : Stream'.Seq α), Stream'.Seq.BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct) →
    f s = g s
-- Init.Prelude
MonadExcept.mk : {ε : outParam (Type u)} →
  {m : Type v → Type w} → ({α : Type v} → ε → m α) → ({α : Type v} → m α → (ε → m α) → m α) → MonadExcept ε m
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasStrictFDerivAt_iff_hasStrictDerivAt`. -/
HasStrictFDerivAt.hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasStrictFDerivAt f f' x → HasStrictDerivAt f (f' 1) x
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The simplex witnessing that `inv` and `hom` compose to the identity  -/
SSet.Edge.InvStruct.invHomId : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    {hom : SSet.Edge x₀ x₁} → (self : hom.InvStruct) → self.inv.CompStruct hom (SSet.Edge.id x₁)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.op_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A), P.op.ι = P.π.op
-- Mathlib.Analysis.Normed.Group.Constructions
norm_ofDual : ∀ {E : Type u_2} [inst : Norm E] (x : Eᵒᵈ), ‖OrderDual.ofDual x‖ = ‖x‖
-- Mathlib.Combinatorics.Quiver.Path
_private.Mathlib.Combinatorics.Quiver.Path.0.Quiver.Path.length.match_1.eq_2 : ∀ {V : Type u_2} [inst : Quiver V] {a : V} (motive : (x : V) → Quiver.Path a x → Sort u_3) (x b : V)
  (p : Quiver.Path a b) (a_1 : b ⟶ x) (h_1 : Unit → motive a Quiver.Path.nil)
  (h_2 : (x b : V) → (p : Quiver.Path a b) → (a_2 : b ⟶ x) → motive x (p.cons a_2)),
  (match x, p.cons a_1 with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons a => h_2 x b p a) =
    h_2 x b p a_1
-- Mathlib.Order.Defs.Unbundled
IsStrictTotalOrder.mk : ∀ {α : Sort u_1} {lt : α → α → Prop} [toTrichotomous : Std.Trichotomous lt] [toIsStrictOrder : IsStrictOrder α lt],
  IsStrictTotalOrder α lt
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a - a = 0 ↔ a ≠ ⊤
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationRightAdjoint_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.evaluationRightAdjoint D c).obj d).map f =
    CategoryTheory.Limits.Pi.lift fun g =>
      CategoryTheory.Limits.Pi.π (fun x => d) (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Order.Kleene
Pi.kstar_def : ∀ {ι : Type u_3} {π : ι → Type u_4} [inst : (i : ι) → KleeneAlgebra (π i)] (a : (i : ι) → π i),
  KStar.kstar a = fun i => KStar.kstar (a i)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.OuterMeasure.coe_fn_injective : ∀ {α : Type u_1}, Function.Injective fun μ s => μ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.getKey! a = t.getKeyD a default