mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelIso.Basic
RelIso.self_trans_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), e.trans e.symm = RelIso.refl r
-- Mathlib.Data.Num.ZNum
Num.div_zero : ∀ (n : Num), n / 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
/-- In a real inner product space, the complex exponential of minus the square of the norm plus
a scalar product is integrable. Useful when discussing the Fourier transform of a Gaussian.  -/
GaussianFourier.integrable_cexp_neg_mul_sq_norm_add : ∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re →
    ∀ (c : ℂ) (w : V),
      MeasureTheory.Integrable (fun v => Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ w v))) MeasureTheory.volume
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.integrable_map_cast_binomial : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval} {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [MeasurableSingletonClass R] (f : R → E),
  MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.darts_isInfix : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₁.IsSubwalk p₂ → p₁.darts <:+: p₂.darts
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.instIteratorSubtypePosNeEndPosOfPure : {m : Type → Type u_1} → {s : String.Slice} → [Pure m] → Std.Iterator s.RevPosIterator m { p // p ≠ s.endPos }
-- Mathlib.Data.PSigma.Order
PSigma.Lex.denselyOrdered_of_noMinOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMinOrder (α i)], DenselyOrdered (Σₗ' (i : ι), α i)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiAlgebraFin.congr_simp : ∀ (R : Type u) (n : ℕ) (A : Type u_1) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [inst_4 : ContinuousMul A],
  ContinuousMultilinearMap.mkPiAlgebraFin R n A = ContinuousMultilinearMap.mkPiAlgebraFin R n A
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOneConst.congr_simp : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1)
  [inst_5 : μ.IsAddHaarMeasure] (p p_1 : ℝ),
  p = p_1 → MeasureTheory.eLpNormLESNormFDerivOneConst μ p = MeasureTheory.eLpNormLESNormFDerivOneConst μ_1 p_1
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.eq_or_eq_of_isPushout : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    ∀ (x₄ : X₄),
      (∃ x₂, (CategoryTheory.ConcreteCategory.hom r) x₂ = x₄) ∨ ∃ x₃, (CategoryTheory.ConcreteCategory.hom b) x₃ = x₄
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAdd : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → Add (ι →₀ M)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An invariant block of a group action is a block.  -/
MulAction.IsInvariantBlock.isBlock : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsInvariantBlock G B → MulAction.IsBlock G B
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- A composition of triangulated adjunctions is triangulated.
 -/
CategoryTheory.Adjunction.IsTriangulated.comp : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ] [adj.CommShift ℤ] {E : Type u_3}
  [inst_15 : CategoryTheory.Category.{v_3, u_3} E] {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D}
  (adj' : F' ⊣ G') [inst_16 : CategoryTheory.Limits.HasZeroObject E] [inst_17 : CategoryTheory.Preadditive E]
  [inst_18 : CategoryTheory.HasShift E ℤ] [inst_19 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive]
  [inst_20 : CategoryTheory.Pretriangulated E] [inst_21 : F'.CommShift ℤ] [inst_22 : G'.CommShift ℤ] [adj'.CommShift ℤ]
  [adj.IsTriangulated] [adj'.IsTriangulated], (adj.comp adj').IsTriangulated
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocsArray.isErased : Lean.Meta.Simp.SimprocsArray → Lean.Name → Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.curriedTensor_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  {X_1 Y : C} (g : X_1 ⟶ Y),
  ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X).map g =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α}, (a == b) = true → m[a]? = m[b]?
-- Init.Data.String.OrderInstances
String.Pos.Raw.instLECiOfNatInt : Lean.Grind.ToInt.LE String.Pos.Raw (Lean.Grind.IntInterval.ci 0)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_uncurry_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D]
  (F : CategoryTheory.Functor B (CategoryTheory.Functor C D)),
  CategoryTheory.Functor.curry.obj (CategoryTheory.Functor.uncurry.obj F) = F
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      Std.Internal.List.minKey (Std.Internal.List.Const.modifyKey k f l) he =
        if (Std.Internal.List.minKey l ⋯ == k) = true then k else Std.Internal.List.minKey l ⋯
-- Aesop.EMap
Aesop.EMap.insertWithM : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      {α : Type} → Lean.Expr → (Option α → m α) → Aesop.EMap α → m (Aesop.EMap α × Option α × α)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.continuousConstSMul_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁], ContinuousConstSMul (M₁ →L[R₁] M₁) M₁
-- Mathlib.Data.Set.Lattice
Set.iUnion_inter_of_antitone : ∀ {ι : Type u_12} {α : Type u_13} [inst : Preorder ι] [IsCodirectedOrder ι] {s t : ι → Set α},
  Antitone s → Antitone t → ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppLid_symm_single_smul : ∀ (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (i : ι × κ) (r : R) (n : N),
  ((finsuppTensorFinsuppLid R N ι κ).symm fun₀ | i => r • n) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => n
-- Mathlib.Topology.Order.OrderClosed
lowerBounds_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] (s : Set α),
  lowerBounds (closure s) = lowerBounds s
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_iInf : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_2} (f : ι → AddSubmonoid M), (iInf f).addUnits = ⨅ i, (f i).addUnits
-- Init.Data.UInt.Lemmas
BitVec.ofNat_uInt64ToNat : ∀ (n : UInt64), BitVec.ofNat 64 n.toNat = n.toBitVec
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.Context.mk : Lean.Expr → Lean.Level → Lean.Expr → Bool → Lean.Expr → Mathlib.Tactic.Abel.Context
-- Aesop.Forward.PremiseIndex
Aesop.instInhabitedPremiseIndex : Inhabited Aesop.PremiseIndex
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The set of additive conjugates of the union of two sets is the union
of the additive conjugates.  -/
AddGroup.addConjugatesOfSet_union : ∀ {G : Type u_5} [inst : AddGroup G] (s t : Set G),
  AddGroup.addConjugatesOfSet (s ∪ t) = AddGroup.addConjugatesOfSet s ∪ AddGroup.addConjugatesOfSet t
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instOne.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], UpperSet.instOne = { one := UpperSet.Ici 1 }
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- The homeomorphism obtained by restricting a `PartialHomeomorph` to a subset of the source.
 -/
PartialHomeomorph.homeomorphOfImageSubsetSource : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialHomeomorph X Y) → {s : Set X} → {t : Set Y} → s ⊆ e.source → ↑e '' s = t → ↑s ≃ₜ ↑t
-- Mathlib.Data.NNReal.Star
instStarModuleNNRealReal : StarModule NNReal ℝ
-- Mathlib.Data.Seq.Computation
Computation.of_results_think : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.think.Results a n → ∃ m, s.Results a m ∧ n = m + 1
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CategoryTheory.Functor.shiftIso.eq_1 : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n a a' : M) (ha' : n + a = a'),
  F.shiftIso n a a' ha' = CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha'
-- Lean.Language.Basic
/-- Reader monad threading a `SnapshotTreeTransform` through `SnapshotTree` construction.  -/
Lean.Language.ToSnapshotTreeM : Type → Type
-- Init.Data.Range.Polymorphic.SInt
Int32.lt.eq_1 : ∀ (a b : Int32), a.lt b = (a.toBitVec.slt b.toBitVec = true)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁_map_mul_of_isTrivial : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} [A.IsTrivial]
  (f : ↥(groupCohomology.cocycles₁ A)) (g h : G), f (g * h) = f g + f h
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclLeftFull : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Join.inclLeft C D).Full
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPoly.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (a b : ℤ)
  (h_1 : (a b : ℤ) → motive (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_1 : Lean.Grind.CommRing.Mon) →
        (a_2 : Lean.Grind.CommRing.Poly) →
          (b : ℤ) →
            (b_1 : Lean.Grind.CommRing.Mon) →
              (b_2 : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add a a_1 a_2) (Lean.Grind.CommRing.Poly.add b b_1 b_2))
  (h_3 : (x x_1 : Lean.Grind.CommRing.Poly) → motive x x_1),
  (match Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b with
    | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => h_1 a b
    | Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
    | x, x_1 => h_3 x x_1) =
    h_1 a b
-- Mathlib.Algebra.Group.Prod
/-- Multiplication as a monoid homomorphism.  -/
mulMonoidHom : {α : Type u_6} → [inst : CommMonoid α] → α × α →* α
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_ofNat : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (n : ℕ) [inst_2 : n.AtLeastTwo],
  (OfNat.ofNat n).coeff = fun₀ | 0 => OfNat.ofNat n
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.const_vadd : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : VAdd γ β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), c +ᵥ f =ᶠ[l] c +ᵥ g
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.picard_apply₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {t₀ : ℝ} {x₀ : E},
  ODE.picard f t₀ x₀ α t₀ = x₀
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_6 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit1, b.bit1 with
    | a, PosNum.one => h_1 a
    | PosNum.one, b => h_2 b
    | a.bit0, b.bit0 => h_3 a b
    | a.bit0, b.bit1 => h_4 a b
    | a.bit1, b.bit0 => h_5 a b
    | a.bit1, b.bit1 => h_6 a b) =
    h_6 a b
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
HasSumUniformlyOn.of_norm_le_summable : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
  {f : α → β → F},
  Summable u → ∀ {s : Set β}, (∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) → HasSumUniformlyOn f (fun x => ∑' (n : α), f n x) s
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.FormalCoproduct C) (m : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) (i : 𝒜)
  (a : (f i).I),
  ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t) m i).f a =
    m.f (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f a)
-- Mathlib.Data.ENNReal.Operations
/-- This lemma has an abbreviated name because it is used frequently.  -/
ENNReal.cancel_of_ne : ∀ {a : ENNReal}, a ≠ ⊤ → AddLECancellable a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.sub_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.sub h').h₂ = h.h₂ - h'.h₂
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f : M →ₗ[R] N), LinearMap.baseChange A f = TensorProduct.AlgebraTensorModule.map LinearMap.id f
-- Mathlib.Data.Seq.Computation
/-- `Computation α` is the type of unbounded computations returning `α`.
An element of `Computation α` is an infinite sequence of `Option α` such
that if `f n = some a` for some `n` then it is constantly `some a` after that.  -/
Computation : Type u → Type u
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function has a limit on its right within a set.  -/
BoundedVariationOn.exists_tendsto_right : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∀ (x : α), ∃ l, Filter.Tendsto f (nhdsWithin x (s ∩ Set.Ioi x)) (nhds l)
-- Init.Data.Array.Range
Array.range'_ne_empty_iff : ∀ {s n step : ℕ}, Array.range' s n step ≠ #[] ↔ n ≠ 0
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together. Stated by permuting the entries of `g`.  -/
Antivary.sum_smul_lt_sum_smul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → (∑ i, f i • g i < ∑ i, f i • g (σ i) ↔ ¬Antivary f (g ∘ ⇑σ))
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forgetCone_π_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T)
  (self : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T)),
  (CategoryTheory.Under.forgetCone X).π.app self = self.hom
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.mk : Std.HashSet (ℕ × Lean.Expr) → Std.HashSet ℕ → Lean.Expr.CollectLooseBVars.State
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.le_of_not_le_of_le : ∀ {α : Type u_1} {hi n lo : α} [inst : LinearOrder α], ¬hi ≤ n → hi ≤ lo → n ≤ lo
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.instT2Space : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A],
  T2Space (Unitization 𝕜 A)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {fallback : β k'} {f : β k → β k},
  (m.modify k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback
-- Mathlib.Order.Category.Frm
Frm.hom_id : ∀ {X : Frm}, Frm.Hom.hom (CategoryTheory.CategoryStruct.id X) = FrameHom.id ↑X
-- Mathlib.Testing.Plausible.Testable
Plausible.Testable.factTestable : {p : Prop} → [Plausible.Testable p] → Plausible.Testable (Fact p)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOpenImmersionInlScheme : ∀ (X Y : AlgebraicGeometry.Scheme), AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.coprod.inl
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily.congr_simp : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] (x x_1 : HahnSeries Γ A),
  x = x_1 →
    ∀ (r r_1 : R),
      r = r_1 → HahnSeries.SummableFamily.binomialFamily x r = HahnSeries.SummableFamily.binomialFamily x_1 r_1
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_head_tail : ∀ {α : Type u} {m : ℕ} (u : Fin m.succ → α), Matrix.vecCons (Matrix.vecHead u) (Matrix.vecTail u) = u
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedString` from a `String` by checking if it's already a valid percent-encoded string.
Returns `some` if valid, `none` otherwise.
 -/
Std.Http.URI.EncodedString.ofString? : {r : UInt8 → Bool} → String → Option (Std.Http.URI.EncodedString r)
-- Lean.Meta.DiscrTree.Util
/-- Fold over the values stored in a `DiscrTree`.
 -/
Lean.Meta.DiscrTree.foldValues : {σ : Type u_1} → {α : Type} → (σ → α → σ) → σ → Lean.Meta.DiscrTree α → σ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, ⊥.arrows = ⊥
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Given an action of a monoidal category `C` on a category `D`,
an action of a monoid object `M` in `C` on an object `X` in `D` is the data of a
map `smul : M ⊙ₗ X ⟶ X` that satisfies unitality and associativity with
multiplication.

See `MulAction` for the non-categorical version.  -/
CategoryTheory.ModObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] → (M : C) → [CategoryTheory.MonObj M] → D → Type v₂
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coePNat : Coe PrimeMultiset (Multiset ℕ+)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_left_sum : ∀ {ι : Type u_1} {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (f : ι → V) (x : E) (s : Finset ι),
  LineDeriv.lineDerivOp (∑ i ∈ s, f i) x = ∑ i ∈ s, LineDeriv.lineDerivOp (f i) x
-- Mathlib.GroupTheory.Index
/-- A subgroup `H` has index two if and only if there exists `a ∉ H` such that for all `b`, one
of `a * b` and `b` belongs to `H`.  -/
Subgroup.index_eq_two_iff_exists_notMem_and' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_empty : ∀ {α : Type u_2} [inst : AddMonoid α], ThreeAPFree ∅
-- Mathlib.CategoryTheory.Sites.Coverage
/-- The two constructions `Coverage.toGrothendieck` and `Coverage.ofGrothendieck` form
a Galois insertion.
 -/
CategoryTheory.Coverage.gi : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    GaloisInsertion CategoryTheory.Coverage.toGrothendieck CategoryTheory.GrothendieckTopology.toCoverage
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_add : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x y : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap (x + y) =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMap x * ↑NumberField.mixedEmbedding.fundamentalCone.expMap y
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.singleRuleTac : Lean.Name → Aesop.RuleTac
-- Std.Http.Data.Status
/-- 226 IM Used
 -/
Std.Http.Status.imUsed : Std.Http.Status
-- Mathlib.Analysis.Normed.Field.Basic
/-- An injective non-unital ring homomorphism from a `DivisionRing` to a `NormedRing` induces a
`NormedDivisionRing` structure on the domain.

See note [reducible non-instances]  -/
NormedDivisionRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : DivisionRing R] →
          [inst_2 : NormedDivisionRing S] →
            [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NormedDivisionRing R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_add : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
-- Mathlib.Data.List.Chain
List.isChain_cons_append_singleton_iff_forall₂ : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a b : α},
  List.IsChain R (a :: l ++ [b]) ↔ List.Forall₂ R (a :: l) (l ++ [b])
-- Mathlib.RingTheory.LaurentSeries
/-- Sending a Laurent series to its `d`-th coefficient is uniformly continuous (independently of the
uniformity with which `K` is endowed).  -/
LaurentSeries.uniformContinuous_coeff : ∀ {K : Type u_2} [inst : Field K] {uK : UniformSpace K} (d : ℤ), UniformContinuous fun f => f.coeff d