mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m z$, where $m$ is a natural number and $z \in M$.  -/
Module.reflection_mul_reflection_pow_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (z : M) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_pow_apply._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) z =
      z +
          (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) +
                Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m / 2)) +
              Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.  -/
CategoryTheory.Functor.PreservesEpimorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.contains_of : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k}, (Std.DTreeMap.Internal.Cell.of k v).contains = true
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.toFreeGroup.eq_1 : ∀ (G : Type u_1) [inst : Group G] [inst_1 : IsFreeGroup G], IsFreeGroup.toFreeGroup G = (IsFreeGroup.mulEquiv G).symm
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_of_forall_one_lt_div_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α},
  (∀ (ε : α), 1 < ε → a / ε ≤ b) → a ≤ b
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsGalois X] (x : (F.obj X).obj),
  (MulAction.stabilizer (CategoryTheory.Aut F) x).Normal
-- Init.Notation
/-- Sequences two computations, allowing the second to depend on the value computed by the first.

If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the result of executing `x` to get
a value of type `α` and then passing it to `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `>>=` in identifiers is `bind`. -/
«term_>>=_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.functorCategory_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J],
  (CategoryTheory.MorphismProperty.isomorphisms C).functorCategory J =
    CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Functor J C)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.mk : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCircuit → p.support.tail.Nodup → p.IsCycle
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_lt : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a < b → Set.uIcc a b = Set.Icc a b
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.iterateEquiv_apply : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  (x : HahnSeries Γ (HahnSeries Γ' R)), HahnSeries.iterateEquiv x = x.ofIterate
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.whisker_π : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f)
  (g : K ≃ J) (k : K), (c.whisker g).π k = c.π (g k)
-- Mathlib.Analysis.Fourier.Convolution
/-- The Fourier transform of the convolution is given by the bilinear map applied to the Fourier
transform of the individual functions.  -/
Real.fourier_bilin_convolution_eq : ∀ {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F₁] [inst_2 : NormedAddCommGroup F₂] [inst_3 : NormedAddCommGroup F₃]
  [inst_4 : InnerProductSpace ℝ E] [inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasurableSpace E] [inst_7 : BorelSpace E]
  [inst_8 : NormedSpace ℂ F₃] [CompleteSpace F₁] [CompleteSpace F₂] [CompleteSpace F₃] [inst_12 : NormedSpace ℂ F₁]
  [inst_13 : NormedSpace ℂ F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) {f₁ : E → F₁} {f₂ : E → F₂},
  MeasureTheory.Integrable f₁ MeasureTheory.volume →
    MeasureTheory.Integrable f₂ MeasureTheory.volume →
      ∀ (ξ : E),
        FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ B MeasureTheory.volume) ξ =
          (B (FourierTransform.fourier f₁ ξ)) (FourierTransform.fourier f₂ ξ)
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgNumLit : Lean.Doc.FromDocArg Lean.NumLit
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.USize.toBitVec_cond : ∀ {c : Bool} {t e : USize}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.tacticDsimp?!_ : Lean.ParserDescr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α},
  (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_inter_add_sdiff : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f s μ → ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_ne_eq_erase' : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  DFinsupp.filter (fun x => i ≠ x) f = DFinsupp.erase i f
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_comm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
        (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
        (CategoryTheory.Functor.commShiftIso F₂ a).hom
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iSup : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C],
  CategoryTheory.ObjectProperty.preservesLimitsOfShape K = ⨅ F, CategoryTheory.ObjectProperty.preservesLimit F
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.run : {α : Type} →
  optParam Bool true →
    optParam Bool true →
      optParam (Array Lean.MVarId) #[] →
        optParam (Array Lean.MVarId) #[] → Lean.Meta.Sym.DefEqM✝ α → Lean.Meta.Sym.SymM α
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_int_mod : ∀ {ι : Type u_1} (s : Finset ι) (n : ℤ) (f : ι → ℤ), (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
-- Init.Data.UInt.Lemmas
USize.ofNatLT_eq_ofNat : ∀ (n : ℕ) {h : n < USize.size}, USize.ofNatLT n h = USize.ofNat n
-- Mathlib.Analysis.LocallyConvex.HahnBanach
ContinuousLinearMap.codRestrict.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f f_1 : M₁ →SL[σ₁₂] M₂)
  (e_f : f = f_1) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p), f.codRestrict p h = f_1.codRestrict p ⋯
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_lt_prod_of_nonempty' : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α]
  [MulLeftStrictMono α] {s : Multiset ι} {f g : ι → α},
  s ≠ ∅ → (∀ i ∈ s, f i < g i) → (Multiset.map f s).prod < (Multiset.map g s).prod
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.finite.inj : ∀ {sign : Float.Model.UnpackedFloat.Sign} {mantissa : ℕ} {exponent : ℤ} {mantissa_pos : 0 < mantissa}
  {sign_1 : Float.Model.UnpackedFloat.Sign} {mantissa_1 : ℕ} {exponent_1 : ℤ} {mantissa_pos_1 : 0 < mantissa_1},
  Float.Model.UnpackedFloat.finite sign mantissa exponent mantissa_pos =
      Float.Model.UnpackedFloat.finite sign_1 mantissa_1 exponent_1 mantissa_pos_1 →
    sign = sign_1 ∧ mantissa = mantissa_1 ∧ exponent = exponent_1
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.mkCategoryAntiquotParserFn : Lean.Name → Lean.Parser.ParserFn
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.WF → t.keys.head? = t.minKey?
-- Mathlib.Topology.MetricSpace.Bounded
Metric.ediam_of_unbounded : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], ¬Bornology.IsBounded s → Metric.ediam s = ⊤
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_pos_iff`. -/
EMetric.diam_pos_iff : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], 0 < Metric.ediam s ↔ s.Nontrivial
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toAddGroup : AddGroup E] →
      [toMetricSpace : MetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖-x + y‖) NormedAddGroup.dist_eq._autoParam → NormedAddGroup E
-- Mathlib.Data.Finset.Image
Finset.map_union : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α),
  Finset.map f (s₁ ∪ s₂) = Finset.map f s₁ ∪ Finset.map f s₂
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_add_left_pos : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α),
  a ∈ s → (s + t).erase a = s.erase a + t
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- See also `setIntegral_rnDeriv_smul'` for a version that requires both measures to be σ-finite,
but doesn't require `s` to be a measurable set.  -/
MeasureTheory.setIntegral_rnDeriv_smul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite μ] {f : α → E},
  μ.AbsolutelyContinuous ν →
    ∀ {s : Set α}, MeasurableSet s → ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.top_ne_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsRegular M rs → ⊤ ≠ Ideal.ofList rs • ⊤
-- Mathlib.RepresentationTheory.Intertwining
/-- Composition of intertwining maps.  -/
Representation.IntertwiningMap.llcomp : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          (ρ : Representation A G V) →
                            (σ : Representation A G W) →
                              (τ : Representation A G U) →
                                σ.IntertwiningMap τ →ₗ[A] ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ
-- Mathlib.LinearAlgebra.Countable
/-- If `R` is countable, then any `R`-submodule spanned by a countable family of vectors is
countable.  -/
Finsupp.instCountableSubtypeMemSubmoduleSpanRange : ∀ {M : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  [Countable R] [Countable ι] (v : ι → M), Countable ↥(Submodule.span R (Set.range v))
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.revlexWF.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) =
    h_1 ()
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.proved : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormSeqResult
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.Nonsingular.eq_of_IsDetpBalanced : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.Nonsingular → A.IsDetpBalanced a b → a = b
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_im : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), RCLike.im ↑r = 0
-- Mathlib.Data.Set.Basic
Set.nonempty_coe_sort : ∀ {α : Type u} {s : Set α}, Nonempty ↑s ↔ s.Nonempty
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioc_of_strictMonoOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictMonoOn f (Set.Icc a b) → f '' Set.Ioc a b = Set.Ioc (f a) (f b)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A category in which coimage-image comparisons are all isomorphisms has images.  -/
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)],
  CategoryTheory.Limits.HasImages C
-- Init.Data.Prod
Prod.snd_swap : ∀ {α : Type u_1} {β : Type u_2} {p : α × β}, p.swap.2 = p.1
-- Std.Sat.AIG.Basic
/-- We always store `.false` at the first position. This allows us to avoid cache lookups
 -/
Std.Sat.AIG.hconst : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (self : Std.Sat.AIG α), self.decls[0] = Std.Sat.AIG.Decl.false
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mulinv-mulinv-mulinv version.  -/
Finset.ruzsa_triangle_inequality_mulInv_mulInv_mulInv : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  (A * C⁻¹).card * B.card ≤ (A * B⁻¹).card * (C * B⁻¹).card
-- Mathlib.Order.Antichain
IsAntichain.preimage_embedding : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β},
  IsAntichain (fun x1 x2 => x1 ≤ x2) t → ∀ (φ : α ↪o β), IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?ₘ_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.get?ₘ t k = Std.Internal.List.getValue? k t.toListModel
-- Aesop.Index.RulePattern
/-- `true` iff the index contains no patterns.  -/
Aesop.RulePatternIndex.isEmpty : Aesop.RulePatternIndex → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.instPartialOrderComponentCompl : {V : Type u} → {G : SimpleGraph V} → {K : Set V} → PartialOrder (G.ComponentCompl K)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The extension of scalars by a composition of commutative ring morphisms
identifies to the composition of the extension of scalars functors.  -/
ModuleCat.extendScalarsComp : {R₁ R₂ R₃ : Type u₁} →
  [inst : CommRing R₁] →
    [inst_1 : CommRing R₂] →
      [inst_2 : CommRing R₃] →
        (f₁₂ : R₁ →+* R₂) →
          (f₂₃ : R₂ →+* R₃) →
            ModuleCat.extendScalars (f₂₃.comp f₁₂) ≅ (ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.eq_2 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (k : ℕ),
  newton_seq_aux✝ hnorm k.succ = ih_n✝ hnorm ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.empty_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (t : Set β), ∅ -ᵥ t = ∅
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_one_add : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑(1 + n) = 1 + ↑n
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Iso.mk_inv_toFun : ∀ {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : β.X), (Pointed.Iso.mk e he).inv.toFun a = e.symm a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) '' Set.Ioc b c = Set.Ico (a / c) (a / b)
-- Mathlib.Order.BoundedOrder.Basic
OrderBot.instSubsingleton : ∀ {α : Type u} [inst : PartialOrder α], Subsingleton (OrderBot α)
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.reflective_products : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Reflective i],
  CategoryTheory.Limits.HasFiniteProducts D
-- Init.Data.UInt.Lemmas
UInt16.ofNatTruncate_finVal : ∀ (n : Fin UInt16.size), UInt16.ofNatClamp ↑n = UInt16.ofFin n
-- Init.Data.Option.Monadic
Option.forIn'_eq_pelim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : (a : α) → a ∈ o → β → m (ForInStep β)) (b : β),
  forIn' o b f = o.pelim (pure b) fun a h => ForInStep.value <$> f a h b
-- Lean.Util.ReplaceLevel
Lean.Expr.replaceLevel : (Lean.Level → Option Lean.Level) → Lean.Expr → Lean.Expr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_insertMany_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, (Std.ExtDHashMap.Const.insertMany m l).size ≤ m.size + l.length
-- Mathlib.Order.WithBot
StrictMono.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f = ∀ ⦃a b : α⦄, a < b → f a < f b
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by adding a constant value to the upper bounds.
 -/
Std.Time.Internal.Bounded.LE.addTop : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → num ≥ 0 → Std.Time.Internal.Bounded.LE n (m + num)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_zero_iff_aestronglyMeasurable : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : TopologicalSpace ε] {f : α → ε}, MeasureTheory.MemLp f 0 μ ↔ MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- the square becomes a pushout square in the category of sheaves of types  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (self : J.MayerVietorisSquare),
  (self.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout
-- Mathlib.Order.Filter.Pointwise
Filter.add_mem_add : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s + t ∈ f + g
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
HasCardinalLT.of_le : ∀ {X : Type u} {κ : Cardinal.{v}}, HasCardinalLT X κ → ∀ {κ' : Cardinal.{v}}, κ ≤ κ' → HasCardinalLT X κ'