mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instMin : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → Min (MeasureTheory.Filtration ι m)
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.iff : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P)
-- Mathlib.Data.Tree.Traversable
BinaryTree.instTraversable : Traversable BinaryTree
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m m_1 : ℕ) (e_m : m = m_1) (k k_1 : ℕ) (e_k : k = k_1) (hn : n = m + k)
  (p p_1 : Polynomial.MonicDegreeEq R n),
  p = p_1 →
    Polynomial.UniversalCoprimeFactorizationRing m k hn p = Polynomial.UniversalCoprimeFactorizationRing m_1 k_1 ⋯ p_1
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.smartHCongr?.forSide : Congr!.Config → Lean.MVarId → Lean.Expr → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Logic.Function.Iterate
Function.Surjective.iterate : ∀ {α : Type u} {f : α → α}, Function.Surjective f → ∀ (n : ℕ), Function.Surjective f^[n]
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ofNat_fst : ∀ {q : ℕ} (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).1 = OfNat.ofNat n
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Expressions of the form `η₁ ⊗ ... ⊗ ηₙ`.  -/
Mathlib.Tactic.BicategoryLike.HorizontalComp : Type
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
-- Mathlib.Condensed.Equivalence
Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite : Stonean.toProfinite.EffectivelyEnough
-- Mathlib.Topology.MetricSpace.Algebra
dist_pair_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] (x₁ x₂ : α) (y : β),
  dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldM_eq_match_step : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : Std.IterM m β},
  Std.IterM.foldM f init it = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, property⟩ => do
        let __do_lift ← f init out
        Std.IterM.foldM f __do_lift it'
      | ⟨Std.IterStep.skip it', property⟩ => Std.IterM.foldM f init it'
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.Topology.Separation.Hausdorff
SeparationQuotient.t2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], T2Space (SeparationQuotient X)
-- Mathlib.Analysis.Normed.Group.Bounded
eventually_cobounded_le_norm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a : ℝ), ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖
-- Mathlib.Data.Set.Basic
Set.not_univ_subset : ∀ {α : Type u} {s : Set α}, ¬Set.univ ⊆ s ↔ ∃ a, a ∉ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : One M} {inst_1 : One N} {toFun : M → N} {map_one' : toFun 1 = 1}
  {toFun_1 : M → N} {map_one'_1 : toFun_1 1 = 1},
  { toFun := toFun, map_one' := map_one' } = { toFun := toFun_1, map_one' := map_one'_1 } → toFun = toFun_1
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with scalar multiplication.  -/
Real.circleAverage_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} [inst_2 : NormedDivisionRing 𝕜]
  [inst_3 : Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] {f : ℂ → E} {c : ℂ} {R : ℝ} {a : 𝕜},
  Real.circleAverage (a • f) c R = a • Real.circleAverage f c R
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform converts right-translation into scalar multiplication by a phase
factor.  -/
Fourier.fourierIntegral_comp_add_right : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : MeasurableSpace 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℂ E] [MeasurableAdd 𝕜] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜)
  [μ.IsAddRightInvariant] (f : 𝕜 → E) (v₀ : 𝕜),
  Fourier.fourierIntegral e μ (f ∘ fun v => v + v₀) = fun w => e (v₀ * w) • Fourier.fourierIntegral e μ f w
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
HasCompactSupport.contDiff_convolution_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G]
  {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {n : ℕ∞},
  HasCompactSupport f →
    ContDiff 𝕜 (↑n) f → MeasureTheory.LocallyIntegrable g μ → ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
-- Mathlib.Algebra.Ring.Defs
IsDomain.toNontrivial : ∀ {α : Type u} {inst : Semiring α} [self : IsDomain α], Nontrivial α
-- Mathlib.Data.Prod.TProd
List.TProd.mk.eq_2 : ∀ {ι : Type u} {α : ι → Type v} (i : ι) (is : List ι), List.TProd.mk (i :: is) = fun f => (f i, List.TProd.mk is f)
-- Mathlib.Data.FP.Basic
FP.RMode : Type
-- Mathlib.Logic.Equiv.Finset
Encodable.mem_sortedUniv : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Encodable α] (x : α), x ∈ Encodable.sortedUniv α
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonJson : Lean.FromJson Lean.Json
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_μ_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.Monoidal] {Z : C}
  (h : (F.obj m₃).obj ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂)).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ m₂).app X)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
        (CategoryTheory.CategoryStruct.comp
          ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X)
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app
              X)
            h)))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β}, (Std.ExtDTreeMap.Const.alter t k f).size ≤ t.size + 1
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
isMIntegralCurveAt_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ}, IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsMIntegralCurveOn γ v s
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.abs_sum_le_sum_abs : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α},
  |s.sum| ≤ (Multiset.map abs s).sum
-- Mathlib.Data.Real.Embedding
Archimedean.embedReal_one : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : One M]
  [inst_4 : ZeroLEOneClass M] [inst_5 : NeZero 1] [inst_6 : Archimedean M], (Archimedean.embedReal M) 1 = 1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocEntry.mk.sizeOf_spec : ∀ (toSimprocOLeanEntry : Lean.Meta.Simp.SimprocOLeanEntry) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc),
  sizeOf { toSimprocOLeanEntry := toSimprocOLeanEntry, proc := proc } = 1 + sizeOf toSimprocOLeanEntry + sizeOf proc
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
`Π i, E →L_c[𝕜] F i` and `E →L_c[𝕜] Π i, F i`.  -/
CompactConvergenceCLM.piEquivL : (𝕜₁ : Type u_1) →
  [inst : NormedField 𝕜₁] →
    (E : Type u_4) →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜₁ E] →
          [inst_3 : TopologicalSpace E] →
            {ι : Type u_7} →
              (F : ι → Type u_8) →
                [inst_4 : (i : ι) → AddCommGroup (F i)] →
                  [inst_5 : (i : ι) → Module 𝕜₁ (F i)] →
                    [inst_6 : (i : ι) → TopologicalSpace (F i)] →
                      [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] →
                        [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜₁ (F i)] →
                          ((i : ι) → CompactConvergenceCLM (RingHom.id 𝕜₁) E (F i)) ≃L[𝕜₁]
                            CompactConvergenceCLM (RingHom.id 𝕜₁) E ((i : ι) → F i)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.ext_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Ring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommGroup E}
  {inst_3 : Module 𝕜 E} {x y : Geometry.SimplicialComplex 𝕜 E}, x = y ↔ x.faces = y.faces
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets_congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.iIndepSets π κ μ ↔ ProbabilityTheory.Kernel.iIndepSets π η μ)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.tail.eq_1 : ∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add a v p_2).tail = p_2
-- Mathlib.Tactic.Qify
/-- `qify` rewrites the main goal by shifting propositions from `ℕ` or `ℤ` to `ℚ`.
This is often useful since `ℚ` has well-behaved subtraction and division.

`qify` makes use of the `@[zify_simps]` and `@[qify_simps]` attributes to insert casts into
propositions, and the `push_cast` tactic to simplify the `ℚ`-valued expressions.

`qify` is in some sense dual to the `lift` tactic. `lift (q : ℚ) to ℤ` will change the type of a
rational number `q` (in the supertype) to `ℤ` (the subtype), given a proof that `q.den = 1`;
propositions concerning `q` will still be over `ℚ`. `qify` changes propositions about `ℕ` or `ℤ`
(the subtype) to propositions about `ℚ` (the supertype), without changing the type of any variable.

* `qify at l1 l2 ...` rewrites at the given locations.
* `qify [h₁, ..., hₙ]` uses the expressions `h₁`, ..., `hₙ` as extra lemmas for simplification.
  This is especially useful in the presence of nat subtraction or of division: passing arguments of
  type `· ≤ ·` or `· ∣ ·` will allow `push_cast` to do more work.

Examples:
```
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  qify
  qify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
  sorry

example (a b c : ℤ) (h : a / b = c) (hab : b ∣ a) (hb : b ≠ 0) : a = c * b := by
  -- Divisibility hypothesis allows pushing `· / ·`.
  qify [hab] at h hb ⊢
  exact (div_eq_iff hb).1 h
```
 -/
Mathlib.Tactic.Qify.qify : Lean.ParserDescr
-- Lean.Message
Lean.MessageDataContext.opts : Lean.MessageDataContext → Lean.Options
-- Mathlib.FieldTheory.Normal.Defs
Normal.splits' : ∀ {F : Type u_1} {K : Type u_2} {inst : Field F} {inst_1 : Field K} {inst_2 : Algebra F K} [self : Normal F K] (x : K),
  (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of `p` in `(p * n)!` is `n` more than that of `n!`.  -/
Nat.Prime.emultiplicity_factorial_mul : ∀ {n p : ℕ}, Nat.Prime p → emultiplicity p (p * n).factorial = emultiplicity p n.factorial + ↑n
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppEquivProdFinsupp_symm_inr : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β),
  (Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y
-- Mathlib.Data.Rat.Cast.Order
Rat.castHom_rat : Rat.castHom ℚ = RingHom.id ℚ
-- Mathlib.Algebra.Free
FreeAddMagma.traverse_eq : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeAddMagma α),
  FreeAddMagma.traverse F x = traverse F x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.diseq_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [Lean.Grind.NoNatZeroDivisors α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_ne_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ ≠ 0 → Lean.Grind.CommRing.Poly.denote ctx p ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffAt_arcsin_iff : ∀ {x : ℝ} {n : WithTop ℕ∞}, ContDiffAt ℝ n Real.arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormal_commutes : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
  [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E] (x : E),
  (algebraMap E K₂) ((χ.restrictNormal E) x) = χ ((algebraMap E K₁) x)
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.CoreHomEquiv.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (homEquiv homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (e_homEquiv : homEquiv = homEquiv_1)
  (homEquiv_naturality_left_symm :
    ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
      (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
  (homEquiv_naturality_right :
    ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
      (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g)),
  { homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
      homEquiv_naturality_right := homEquiv_naturality_right } =
    { homEquiv := homEquiv_1, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
/-- If `F` reflects pushouts, then it reflects epimorphisms.  -/
CategoryTheory.reflects_epi_of_reflectsColimit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f f) F] [CategoryTheory.Epi (F.map f)],
  CategoryTheory.Epi f
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_intro : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α},
  (∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) → μ₁ ≤ μ₂
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : Mathlib.Tactic.Coherence.LiftObj X] →
        Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.CategoryStruct.id X)
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The separable degree divides the degree, in function of the exponential characteristic of F.  -/
Polynomial.IsSeparableContraction.dvd_degree' : ∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f g : Polynomial F},
  Polynomial.IsSeparableContraction q f g → ∃ m, g.natDegree * q ^ m = f.natDegree
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α), a ∈ MulAction.orbit G (g • a)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_3.splitter : (motive : ONote × ℕ → Sort u_1) →
  (o₁ : ONote × ℕ) →
    (Unit → motive (ONote.zero, 0)) →
      (Unit → motive (ONote.zero, 1)) →
        ((m : ℕ) → (m = 0 → False) → motive (ONote.zero, m.succ)) →
          ((a0 : ONote) → (a : ℕ+) → (a_1 : ONote) → (m : ℕ) → motive (a0.oadd a a_1, m)) → motive o₁
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_eq_inter_Ico : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ), Dynamics.dynEntourage T U n = ⋂ k, (Prod.map T T)^[↑k] ⁻¹' U
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.pow_Uniformizer_is_pow_generator : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] (π : v.Uniformizer) (n : ℕ),
  IsLocalRing.maximalIdeal ↥v.valuationSubring ^ n = Ideal.span {π.val ^ n}
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.isoMk_inv_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X}
  (hr : f.right ≅ g.right)
  (hw : autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) CategoryTheory.Under.isoMk._auto_1),
  (CategoryTheory.Under.isoMk hr hw).inv.right = hr.inv
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.sub_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f g : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0)
  (hg : CategoryTheory.CategoryStruct.comp (R.complex.d m n) g = 0),
  R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.eq_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) {x : N} {y : M}, y = e.symm x ↔ e y = x
-- Mathlib.Data.Analysis.Filter
CFilter.mk.sizeOf_spec : ∀ {α : Type u_1} {σ : Type u_2} [inst : PartialOrder α] [inst_1 : SizeOf α] [inst_2 : SizeOf σ] (f : σ → α) (pt : σ)
  (inf : σ → σ → σ) (inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a) (inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b),
  sizeOf { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right } = 1 + sizeOf pt
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_subset_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal}, ε₁ ≤ ε₂ → Metric.eball x ε₁ ⊆ Metric.eball x ε₂
-- Lean.Util.SCC
Lean.SCC.State.nextIndex : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SCC.State α → ℕ
-- Mathlib.Data.List.SplitBy
List.ne_nil_of_mem_splitBy : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α}, m ∈ List.splitBy r l → m ≠ []
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_toSubsemigroup : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ), H.unop.toSubsemigroup = H.unop
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mapComp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.mapComp F G).hom.app X =
    (match X with
      | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a)))
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_absolutelyContinuous : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  (μ.withDensity f).AbsolutelyContinuous μ
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.mem_range_self : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  (x : M), f x ∈ f.range
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- When `J` is a well-ordered type, `F : Jᵒᵖ ⥤ Type v`, and `d : F.WellOrderInductionData`,
this is the section of `F` that is determined by `val₀ : F.obj (op ⊥)`  -/
CategoryTheory.Functor.WellOrderInductionData.sectionsMk : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        F.WellOrderInductionData → [inst_2 : OrderBot J] → [WellFoundedLT J] → F.obj (Opposite.op ⊥) → ↑F.sections
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_id : ∀ {P : Type u_3} [inst : AddZeroClass P] (S : AddSubmonoid P), AddSubmonoid.comap (AddMonoidHom.id P) S = S
-- Std.Sync.Broadcast
Std.Broadcast.Error.ofNat_ctorIdx : ∀ (x : Std.Broadcast.Error), Std.Broadcast.Error.ofNat x.ctorIdx = x
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.final_snd_of_isFiltered_structuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B]
  [∀ (a : A), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow (L.obj a) R)],
  (CategoryTheory.Comma.snd L R).Final
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.fun_sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
  [MeasurableSub₂ G], Measurable f → Measurable g → Measurable fun i => f i - g i
-- Mathlib.Analysis.Quaternion
Quaternion.coeComplex_add : ∀ (z w : ℂ), ↑(z + w) = ↑z + ↑w
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.ne_zero : ∀ {n : ℕ}, Nat.Prime n → n ≠ 0
-- Mathlib.Control.Applicative
instApplicativeConstOfOneOfMul : {α : Type u_1} → [One α] → [Mul α] → Applicative (Functor.Const α)
-- Init.Data.UInt.Lemmas
UInt16.neg_mul_comm : ∀ (a b : UInt16), -a * b = a * -b
-- Mathlib.Order.Closure
ClosureOperator.le_closure_iff : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α} {x y : α}, x ≤ c y ↔ c x ≤ c y
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_fromSubtype : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j)
      (CategoryTheory.Limits.biproduct.fromSubtype f p) =
    CategoryTheory.Limits.biproduct.ι f ↑j