mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.Tactic
/-- `modifyTarget mvarId f` updates the target of the metavariable `mvarId` with
`f`. For any `e`, `f e` must be defeq to `e`. If `mvarId` does not refer to
a declared metavariable, nothing happens.
 -/
Mathlib.Tactic.modifyTarget : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → (Lean.Expr → Lean.Expr) → m Unit
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- `reverse` acts only on the right of the tensor product.  -/
CliffordAlgebra.toBaseChange_reverse : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (x : CliffordAlgebra (QuadraticForm.baseChange A Q)),
  (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.reverse x) =
    (TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ((CliffordAlgebra.toBaseChange A Q) x)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_mul_cancel_of_fmod_eq_zero : ∀ {a b : ℤ}, a.fmod b = 0 → a.fdiv b * b = a
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_mul_symm_re_eq_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y * inner 𝕜 y x) = ‖inner 𝕜 x y * inner 𝕜 y x‖
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
_private.Mathlib.RingTheory.Polynomial.UniversalFactorizationRing.0.Polynomial.term𝓡 : Lean.ParserDescr
-- Mathlib.RingTheory.Perfection
/-- The valuation `Perfection(O/(p)) → ℝ≥0`.
Given `f ∈ Perfection(O/(p))`, if `f = 0` then output `0`;
otherwise output `preVal(f(n))^(p^n)` for any `n` such that `f(n) ≠ 0`.  -/
PreTilt.val : (K : Type u₁) →
  [inst : Field K] →
    (v : Valuation K NNReal) →
      (O : Type u₂) →
        [inst_1 : CommRing O] →
          [inst_2 : Algebra O K] →
            v.Integers O →
              (p : ℕ) → [inst : Fact (Nat.Prime p)] → [inst_3 : Fact ¬IsUnit ↑p] → Valuation (PreTilt O p) NNReal
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α} (h : t.WF),
  (Std.TreeMap.Raw.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x t[x]).getD fallback
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCancelMonoid (f i)],
  Pi.addCancelMonoid = { toAddLeftCancelMonoid := Pi.addLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instSupSet : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → SupSet ↥L
-- Init.Data.List.Lemmas
List.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ List.replicate n a → b = a
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instInvCoeOfInvMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Inv (R i)] →
              [∀ (i : ι), InvMemClass (S i) (R i)] → Inv (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.hasLimit_of_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D)
  (E : CategoryTheory.Functor D C) [E.IsEquivalence] [CategoryTheory.Limits.HasLimit (K.comp E)],
  CategoryTheory.Limits.HasLimit K
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.alter m k f) k = f (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.limsup_eq_sInf_univ_of_empty : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → ∀ (i : ι'), p i → s i = ∅ → Filter.limsup f v = sInf Set.univ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_const_left : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (c : β) (X : Ω → β'),
  ProbabilityTheory.IndepFun (fun x => c) X μ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.antisymm : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₁ → L₁ = L₂
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instIsZeroApplyReal : ∀ {E : Type u_3} [inst : AddGroup E], IsZeroApply (NonarchAddGroupSeminorm E) E ℝ
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_eq_add_neg : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (a b : α), a - b = a + -b
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `y * x`.  -/
IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x y : R)
  [IsLocalization.Away x S], IsLocalization.Away (y * x) (Localization.Away ((algebraMap R S) y))
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductive principle used to prove propositions about the elements of a quotient by a
congruence relation.  -/
Con.induction_on : ∀ {M : Type u_1} [inst : Mul M] {c : Con M} {C : c.Quotient → Prop} (q : c.Quotient), (∀ (x : M), C ↑x) → C q
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_unitIso : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (J → C))
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
/-- The `TensorAlgebra` of a free module over an integral domain is a domain.  -/
SymmetricAlgebra.instIsDomain : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.Free R M], IsDomain (SymmetricAlgebra R M)
-- Mathlib.Data.NNRat.Floor
NNRat.ceil_cast : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (x : ℚ≥0), ⌈↑x⌉₊ = ⌈x⌉₊
-- Init.Data.UInt.Lemmas
UInt8.sub_neg : ∀ {a b : UInt8}, a - -b = a + b
-- Lean.DocString.Parser
/-- Parses as `ifVerso` if module docs should use Verso syntax, or as `ifNotVerso` otherwise.
Checks `doc.verso.module` if explicitly set, otherwise falls back to `doc.verso`.
 -/
Lean.Doc.Parser.ifVersoModuleDocsFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Algebra.Hom
IsScalarTower.coe_toAlgHom' : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  ⇑(IsScalarTower.toAlgHom R S A) = ⇑(algebraMap S A)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_def : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (x : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign x =
    match w, x with
    | w, Std.Tactic.BVDecide.BVExpr.var idx =>
      have packedBv := assign.get idx;
      if h : packedBv.w = w then h ▸ packedBv.bv else BitVec.truncate w packedBv.bv
    | w, Std.Tactic.BVDecide.BVExpr.const val => val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr =>
      BitVec.extractLsb' start len (Std.Tactic.BVDecide.BVExpr.eval assign expr)
    | w, lhs.bin op rhs =>
      op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)
    | w, lhs.append rhs h =>
      ⋯ ▸ (Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs)
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h =>
      ⋯ ▸ BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
    | w, lhs.shiftLeft rhs => Std.Tactic.BVDecide.BVExpr.eval assign lhs <<< Std.Tactic.BVDecide.BVExpr.eval assign rhs
    | w, lhs.shiftRight rhs => Std.Tactic.BVDecide.BVExpr.eval assign lhs >>> Std.Tactic.BVDecide.BVExpr.eval assign rhs
    | w, lhs.arithShiftRight rhs =>
      (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.Probability.Kernel.Category.Stoch
instIsStableUnderBraidingSFinKerStochHom : StochHom.IsStableUnderBraiding
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map_π_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F'] (f : F ⟶ F')
  (j : J) {Z : C} (h : (F'.obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F' j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j)
      (CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j) h)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro.sizeOf_spec : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (a : F.A) (a_1 : F.B a → PFunctor.Approx.CofixA F n),
  sizeOf (PFunctor.Approx.CofixA.intro a a_1) = 1 + sizeOf n + sizeOf a
-- Mathlib.Order.Max
NoTopOrder.mk : ∀ {α : Type u_3} [inst : LE α], (∀ (a : α), ∃ b, ¬b ≤ a) → NoTopOrder α
-- Plausible.Arbitrary
/-- This can be specialized into customized `Arbitrary Char` instances.
The resulting instance has `1 / p` chances of making an unrestricted choice of characters
and it otherwise chooses a character from `chars` with uniform probability.  -/
Plausible.Char.arbitraryFromList : ℕ → (chars : List Char) → 0 < chars.length → Plausible.Arbitrary Char
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- This uses `p` instead of `q` when `i = p.length` unlike the unprimed version.  -/
SimpleGraph.Walk.getVert_append' : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ),
  (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.transpose.row = A.col
-- Mathlib.Order.Disjoint
IsCompl.inf_left_eq_bot_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl y z → (x ⊓ y = ⊥ ↔ x ≤ z)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrictOfInjective.congr_simp : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f f_1 : M₁ →ₗ[R] M₂) (e_f : f = f_1) (i i_1 : M₃ →ₗ[R] M₂) (e_i : i = i_1)
  (hi : Function.Injective ⇑i) (hf : ∀ (x : M₁), f x ∈ i.range),
  f.codRestrictOfInjective i hi hf = f_1.codRestrictOfInjective i_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_id_comp : ∀ (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₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂))
        (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₁ F₂)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
-- Mathlib.Data.Int.Cast.Basic
Int.cast_three : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑3 = 3
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {V W : BialgCat R} (toBialgHom' toBialgHom'_1 : V.carrier →ₐc[R] W.carrier),
  ({ toBialgHom' := toBialgHom' } = { toBialgHom' := toBialgHom'_1 }) = (toBialgHom' = toBialgHom'_1)
-- Mathlib.Order.SuccPred.Archimedean
LE.le.exists_succ_iterate : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {a b : α},
  a ≤ b → ∃ n, Order.succ^[n] a = b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_left : ∀ {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m), Fin.append u v (Fin.castAdd n i) = u i
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- If two functions agree in a neighborhood, then so do their iterated derivatives.  -/
Filter.EventuallyEq.iteratedDeriv : ∀ {𝕜 : Type u_7} [inst : NontriviallyNormedField 𝕜] {F : Type u_8} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₁ f₂ : 𝕜 → F} {x : 𝕜},
  f₁ =ᶠ[nhds x] f₂ → ∀ (n : ℕ), iteratedDeriv n f₁ =ᶠ[nhds x] iteratedDeriv n f₂
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_dvd_subst : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ)
  (p₂ : Int.Internal.Linear.Poly) (d₃ : ℤ) (p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_dvd_subst_cert x p₁ d₂ p₂ d₃ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      d₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂ → d₃ ∣ Int.Internal.Linear.Poly.denote' ctx p₃
-- Mathlib.Analysis.Complex.Hadamard
/-- A function useful for the proofs steps. We will aim to show that it is bounded by 1.  -/
Complex.HadamardThreeLines.F : {E : Type u_1} → [inst : NormedAddCommGroup E] → (ℂ → E) → [NormedSpace ℂ E] → ℝ → ℂ → E
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.accept.sizeOf_spec : ∀ {ctx : Type u_1} [inst : SizeOf ctx] (context : ctx),
  sizeOf (Mathlib.TacticAnalysis.TriggerCondition.accept context) = 1 + sizeOf context
-- Mathlib.Topology.Homotopy.HSpaces
Path.continuous_delayReflLeft : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X}, Continuous fun p => Path.delayReflLeft p.1 p.2
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_neg_vadd_sdiff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ ((-c +ᵥ s) \ t) = μ (s \ (c +ᵥ t))
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.mk.sizeOf_spec : ∀ (unfolds : Lean.NameMap Lean.Meta.SimpTheorem) (casts : Lean.NameMap (Lean.Name × Lean.Name))
  (insertionFuns : Lean.NameSet),
  sizeOf { unfolds := unfolds, casts := casts, insertionFuns := insertionFuns } =
    1 + sizeOf unfolds + sizeOf casts + sizeOf insertionFuns
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.isHenstock_toSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).IsHenstock
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Every continuous representation "is" a representation.  -/
ContRepresentation.toRepresentation : (R : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] →
                [inst_5 : Module R V] → ContRepresentation R G V → Representation R G V
-- Mathlib.GroupTheory.OrderOfElement
orderOf_ofAdd_eq_addOrderOf : ∀ {α : Type u_6} [inst : AddMonoid α] (a : α), orderOf (Multiplicative.ofAdd a) = addOrderOf a
-- Mathlib.Probability.Distributions.Uniform
PMF.toOuterMeasure_uniformOfFinset_apply : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (t : Set α),
  (PMF.uniformOfFinset s hs).toOuterMeasure t = ↑{x ∈ s | x ∈ t}.card / ↑s.card
-- Mathlib.Order.Booleanisation
Booleanisation.LE.comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  a ≤ b → (Booleanisation.comp b).LE (Booleanisation.comp a)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.openPartialHomeomorph.congr_simp : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] (c : ChartedSpaceCore H M) (e e_1 : PartialEquiv M H)
  (e_e : e = e_1) (he : e ∈ c.atlas), c.openPartialHomeomorph e he = c.openPartialHomeomorph e_1 ⋯
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_mul : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M) (x y : ↥S), ↑(x * y) = ↑x * ↑y
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVeq : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.veq ValuativeRel.veq ValuativeRel.veq
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- If two functions agree in a neighborhood of `x`, then one is harmonic at `x` iff so is the other.
 -/
InnerProductSpace.harmonicAt_congr_nhds : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  f₁ =ᶠ[nhds x] f₂ → (InnerProductSpace.HarmonicAt f₁ x ↔ InnerProductSpace.HarmonicAt f₂ x)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZero P] {g : N →+ P}
  {f₁ f₂ : M →+ N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Analysis.Convex.StrictCombination
centerMass_mem_ball_of_strictConvexSpace : ∀ {V : Type u_2} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  {t : Finset ι} {w : ι → ℝ} {p : V} {r : ℝ} {z : ι → V},
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ {i j : ι},
      i ∈ t →
        j ∈ t →
          z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ Metric.closedBall p r) → t.centerMass w z ∈ Metric.ball p r
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_cocompact_atTop : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] [ProperSpace E], Filter.Tendsto norm (Filter.cocompact E) Filter.atTop
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given an `AddMonoid` homomorphism `f` from `M` to `P`, the kernel of `f`
is the unique additive congruence relation on `M` whose induced map from the quotient of `M`
to `P` is injective.  -/
AddCon.ker_eq_lift_of_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f : M →+ P)
  (H : c ≤ AddCon.ker f), Function.Injective ⇑(c.lift f H) → AddCon.ker f = c
-- Std.Http.Data.Method
/-- Create a calendar collection.
Source: https://www.rfc-editor.org/rfc/rfc4791#section-5.3.1
 -/
Std.Http.Method.mkcalendar : Std.Http.Method
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_star : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : StarAddMonoid β] [inst_4 : ContinuousStar β] (f : CompactlySupportedContinuousMap α β), ⇑(star f) = star ⇑f
-- Mathlib.Tactic.Linarith.Frontend
/-- If `e` is a comparison `a R b` or the negation of a comparison `¬ a R b`, found in the target,
`getContrLemma e` returns the name of a lemma that will change the goal to an
implication, along with the type of `a` and `b`.

For example, if `e` is `(a : ℕ) < b`, returns ``(`lt_of_not_ge, ℕ)``.
 -/
Mathlib.Tactic.Linarith.getContrLemma : Lean.Expr → Lean.MetaM (Lean.Name × Lean.Expr)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_apply_eq_zero_iff`. -/
Submodule.linearProjOfIsCompl_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) {x : E}, (p.projectionOnto q h) x = 0 ↔ x ∈ q
-- Mathlib.Algebra.Group.Defs
pow_zero : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 0 = 1
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_add : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C₁ C₂ : ConvexCone R M} {x : M}, x ∈ C₁ + C₂ ↔ ∃ y ∈ C₁, ∃ z ∈ C₂, y + z = x
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.germ_stalkToLocalizationₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.structurePresheafInModuleCat R M).germ U x hx)
      (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x) =
    AlgebraicGeometry.StructureSheaf.openToLocalizationₗ✝ R M U x hx
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.instReprExpr_lean : Repr Int.Internal.Linear.Expr
-- Mathlib.Topology.Defs.Basic
/-- A predicate saying that a set is an open set. Use `IsOpen` in the root namespace instead.  -/
TopologicalSpace.IsOpen : {X : Type u} → [self : TopologicalSpace X] → Set X → Prop
-- Init.Data.Option.Lemmas
Option.max_eq_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Max α],
  (∀ (x y : α), y ≤ x → x ⊔ y = x) → ∀ {a b : Option α}, b ≤ a → a ⊔ b = a
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app : ∀ {X Y Z : AlgebraicGeometry.Scheme} {M : X.Modules} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).inv.app M) U =
    CategoryTheory.CategoryStruct.id
      (((AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.comp f g)).obj M).presheaf.obj
        (Opposite.op U))
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Every entry of a column stochastic matrix is less than or equal to 1.  -/
Matrix.le_one_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n → ∀ {i j : n}, M j i ≤ 1
-- Mathlib.Analysis.Normed.Group.Continuity
Inseparable.nnnorm_eq_nnnorm' : ∀ {E : Type u_4} [inst : SeminormedGroup E] {u v : E}, Inseparable u v → ‖u‖₊ = ‖v‖₊
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two
`weightedVSubOfPoint` expressions.  -/
Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₁ p₂ : ι → P) (b : P),
  ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSubOfPoint p₁ b) w - (s.weightedVSubOfPoint p₂ b) w
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_nat_mul_pi : ∀ (n : ℕ), Complex.tan (↑n * ↑Real.pi) = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_half_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ},
  ∀ y ∈ Metric.ball x (ε / 2), Metric.ball y (ε / 2) ⊆ Metric.ball x ε