mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.inr.eq_1 : ∀ (R : Type u_1) [inst : Semiring R] (M₁ : Type u_2) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] (M₂ : Type u_3) [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ContinuousLinearMap.inr R M₁ M₂ = ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R M₂)
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift_galRestrict' : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] (σ : L →ₐ[K] L₂),
  galLift K L L₂ (galRestrict' A B B₂ σ) = σ
-- Mathlib.Algebra.Ring.Defs
add_sq : ∀ {α : Type u} [inst : CommSemiring α] (a b : α), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
-- Mathlib.CategoryTheory.Category.Init
/-- Log a message whenever the category theory discharger uses `grind`.  -/
mathlib.tactic.category.log_grind : Lean.Option Bool
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instCharZero : ∀ {d : ℤ}, CharZero (ℤ√d)
-- Init.Data.Ord.Basic
Ordering.isGE_swap : ∀ {o : Ordering}, o.swap.isGE = o.isLE
-- Mathlib.Algebra.Group.Basic
mul_ne_left : ∀ {M : Type u_4} [inst : Monoid M] [IsLeftCancelMul M] {a b : M}, a * b ≠ a ↔ b ≠ 1
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.unop_mono_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : Cᵒᵖ} (f : B ⟶ A) [CategoryTheory.Epi f],
  CategoryTheory.Mono f.unop
-- Lean.Elab.DefView
/-- Unstructured syntax object comprising the full "header" of the definition from the modifiers
(incl. docstring) up to the value, used for determining header elaboration reuse.
 -/
Lean.Elab.DefParsed.fullHeaderRef : Lean.Elab.DefParsed → Lean.Syntax
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {x y : C} (f : x ⟶ y),
  W f → W.multiplicativeClosure' f
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The isomorphism `(((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b'` when `b' = b + y`.  -/
HomologicalComplex₂.shiftFunctor₂XXIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) →
        (a b y b' : ℤ) → b' = b + y → ((((HomologicalComplex₂.shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b')
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.map f m) k = (Option.map (f k) (Std.ExtDHashMap.Const.get? m k)).get!
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.overToCoalgebra_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (f : CategoryTheory.Over X),
  ((CategoryTheory.overToCoalgebra X).obj f).a =
    CategoryTheory.Limits.prod.lift f.hom (CategoryTheory.CategoryStruct.id f.left)
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- Asymptotically, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of
the characteristic functions of `f` and `g`, respectively.
 -/
ValueDistribution.characteristic_add_top_eventuallyLE : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f₁ f₂ : ℂ → E},
  Meromorphic f₁ →
    Meromorphic f₂ →
      ValueDistribution.characteristic (f₁ + f₂) ⊤ ≤ᶠ[Filter.atTop]
        ValueDistribution.characteristic f₁ ⊤ + ValueDistribution.characteristic f₂ ⊤ + fun x => Real.log 2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastReplicate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig newWidth) (assign : α → Bool) (idx : ℕ)
  (hidx : idx < newWidth),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate aig target).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := target.inner.get (idx % target.w) ⋯ }⟧
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.ExtremalEpi.subobject_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.ExtremalEpi f]
  {A : CategoryTheory.Subobject Y}, A.Factors f → A = ⊤
-- Mathlib.Analysis.Normed.Group.Ultra
/-- A commutative group with an ultrametric group seminorm is nonarchimedean (as a topological
group, i.e. every neighborhood of 1 contains an open subgroup).  -/
IsUltrametricDist.nonarchimedeanGroup : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] [IsUltrametricDist M], NonarchimedeanGroup M
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.nontrivial_iff : ∀ {R : Type u} [inst : Semiring R], Nontrivial (Polynomial R) ↔ Nontrivial R
-- Std.Http.Data.URI.Basic
Std.Http.instInhabitedURI.default : Std.Http.URI
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_inv_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (e : A ≅ B) (x : ↑B),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Std.Async.Timer
/-- Return a `Selector` that completes after `duration`.
 -/
Std.Async.Selector.sleep : Std.Time.Millisecond.Offset → Std.Async.Async (Std.Async.Selector Unit)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Order.Defs.Unbundled
equivalence_iff_isEquiv : ∀ {α : Sort u_1} (lt : α → α → Prop), Equivalence lt ↔ IsEquiv α lt
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.mul_star_self_of_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ pinGroup Q → x * star x = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.get! a =
    if h : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get! a
-- Lean.Elab.Term.TermElabM
/-- Executes `x` in the context of the given declaration name. Ensures that the info tree is set up
correctly and adjusts the declaration name generator to generate names below this name, resetting
the nested counter.
 -/
Lean.Elab.Term.withDeclName : {α : Type} → Lean.Name → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The localization of an integral domain at the complement of a prime ideal is an integral domain.
 -/
IsLocalization.isDomain_of_local_atPrime : ∀ {A : Type u_4} [inst : CommRing A] [IsDomain A] {P : Ideal A} (x : P.IsPrime), IsDomain (Localization.AtPrime P)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.dest.eq_1 : ∀ {F : Type u → Type u} [q : QPF F], QPF.Fix.dest = QPF.Fix.rec (Functor.map QPF.Fix.mk)
-- Mathlib.Geometry.Manifold.StructureGroupoid
mem_pregroupoid_of_eqOnSource : ∀ {H : Type u_1} [inst : TopologicalSpace H] (PG : Pregroupoid H) {e e' : OpenPartialHomeomorph H H},
  e ≈ e' → PG.property (↑e) e.source → PG.property (↑e') e'.source
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `isAtom_dual_iff_isCoatom`. -/
IsCoatom.dual : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → IsAtom (OrderDual.toDual a)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (t : Set α) {p : α → Prop},
  (∀ᵐ (x : α) ∂μ.restrict t, p x) → (∀ᵐ (x : α) ∂μ.restrict tᶜ, p x) → ∀ᵐ (x : α) ∂μ, p x
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] (c : NNReal), (c • μ).InnerRegularCompactLTTop
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- If a set of vertices `A` is an `n`-clique in subgraph of `G` induced by a superset of `A`,
its embedding is an `n`-clique in `G`.  -/
SimpleGraph.IsNClique.of_induce : ∀ {α : Type u_1} {G : SimpleGraph α} {S : G.Subgraph} {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ},
  (S.induce F).coe.IsNClique n s → G.IsNClique n (Finset.map { toFun := Subtype.val, inj' := ⋯ } s)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_natCast : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (n : ℕ), Polynomial.map f ↑n = ↑n
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.eval₂_expand : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) (f : R →+* S)
  (g : σ → S) (φ : MvPolynomial σ R),
  MvPolynomial.eval₂ f g ((MvPolynomial.expand p) φ) = MvPolynomial.eval₂ f (g ^ p) φ
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- Evaluate a polynomial `p : PolynomialModule R M` at `r : R`.  -/
PolynomialModule.eval : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → R → PolynomialModule R M →ₗ[R] M
-- Init.Data.Int.Order
Int.instIsLinearOrder : Std.IsLinearOrder ℤ
-- Mathlib.Probability.ConditionalProbability
/-- **Bayes' Theorem**  -/
ProbabilityTheory.cond_eq_inv_mul_cond_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ], μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t
-- Init.Data.List.Nat.TakeDrop
List.takeWhile_eq_take_findIdx_not : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.takeWhile p xs = List.take (List.findIdx (fun a => !p a) xs) xs
-- Mathlib.Order.Filter.Prod
Filter.prod_mem_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : Filter α} {g : Filter β}, s ∈ f → t ∈ g → s ×ˢ t ∈ f ×ˢ g
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A `SubMulAction` of a `MulAction` is a `MulAction`.  -/
SubMulAction.SMulMemClass.toMulAction : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] →
      [inst_1 : MulAction R M] →
        {A : Type u_1} → [inst_2 : SetLike A M] → [hA : SMulMemClass A R M] → (S' : A) → MulAction R ↥S'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Note this also holds for `z = 0`, but we do not need this case for `sin_pi_mul_eq`.  -/
EulerSine.integral_cos_mul_cos_pow : ∀ {z : ℂ} {n : ℕ},
  2 ≤ n →
    z ≠ 0 →
      (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n =
        (↑n - 1) / ↑n * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hf : S.f = 0),
  (S.cyclesIsoLeftHomology hf).hom = S.leftHomologyπ
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.stronglyMeasurable_gaussianPDFReal : ∀ (μ : ℝ) (v : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.gaussianPDFReal μ v)
-- Mathlib.Data.Set.Image
Set.image_preimage_inter : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The obvious extra degeneracy on the standard simplex.  -/
SSet.Augmented.StandardSimplex.extraDegeneracy : (Δ : SimplexCategory) → CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy (SSet.Augmented.stdSimplex.obj Δ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w start : ℕ} {assign : α → Bool} {inv : Bool}
  (aig : Std.Sat.AIG α) (curr : ℕ) (xc : aig.RefVec w) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := curr, x := xc }).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Constant functions are harmonic
 -/
InnerProductSpace.harmonicOnNhd_const : ∀ {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] {s : Set E} (c : F),
  InnerProductSpace.HarmonicOnNhd (fun x => c) s
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance2.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (c : RBTree.RBNode α) (z : α) (d_1 : RBTree.RBNode α), d = RBTree.RBNode.node RBTree.RBColor.red c z d_1 → False) →
    (match a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d with
      | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) =>
        h_1 a x b y c z d
      | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d =>
        h_2 a x b y c z d
      | a, x, b => h_3 a x b) =
      h_2 a x b y c z d
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addRightStrictMono : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] [AddRightStrictMono M],
  AddRightStrictMono { x // 0 < x }
-- Mathlib.Util.Delaborators
/-- Dependent function type (a "pi type"). The notation `Π x ∈ s, β x` is
short for `Π x, x ∈ s → β x`.  -/
PiNotation.«termΠ__,_» : Lean.ParserDescr
-- Mathlib.Topology.Instances.Real.Lemmas
/-- An antitone, bounded below sequence `f : ℕ → ℝ` on `Ici k` has the finite
limit `sInf (f '' Ici k)`.  -/
Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici : ∀ {f : ℕ → ℝ} {k : ℕ},
  AntitoneOn f (Set.Ici k) → BddBelow (f '' Set.Ici k) → Filter.Tendsto f Filter.atTop (nhds (sInf (f '' Set.Ici k)))
-- Mathlib.Tactic.Ring.RingNF
/-- `ring` solves equations in *commutative* (semi)rings, allowing for variables in the
exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be
suggested. See also `ring1`, which fails if the goal is not an equality.

* `ring!` will use a more aggressive reducibility setting to determine equality of atoms.

Examples:
```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
```
 -/
Mathlib.Tactic.RingNF.ring : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.subset_subsetSum : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M}, A ⊆ A.subsetSum
-- Aesop.Forward.Substitution
Aesop.instInhabitedSubstitution.default : Aesop.Substitution
-- Mathlib.Order.Filter.Map
Filter.mem_kernMap : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β},
  s ∈ Filter.kernMap m f ↔ ∃ t ∈ f, Set.kernImage m t = s
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∑ j ∈ s, f j) (f i) κ μ
-- Mathlib.Data.Num.ZNum
/-- This tactic tries to turn an (in)equality about `ZNum`s to one about `Int`s by rewriting.
```lean
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer_rw
  exact le_add_of_nonneg_right (mul_self_nonneg _)
```
 -/
ZNum.transfer_rw : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.bipartiteDoubleCover.match_1.congr_eq_1 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (x x_1 : V ⊕ V)
  (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w')) (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w'))
  (h_3 : (x x_2 : V ⊕ V) → motive x x_2) (v' w' : V),
  x = Sum.inl v' →
    x_1 = Sum.inr w' →
      (match x, x_1 with
        | Sum.inl v', Sum.inr w' => h_1 v' w'
        | Sum.inr v', Sum.inl w' => h_2 v' w'
        | x, x_2 => h_3 x x_2) ≍
        h_1 v' w'
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf),
  (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).K = kf.pt
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_fun' : ∀ {R : Type u} {η : Type u₁'} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Fintype η],
  Module.rank R (η → R) = ↑(Fintype.card η)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- `M^~` as a sheaf of `𝒪_{Spec R}`-modules
 -/
AlgebraicGeometry.tilde : {R : CommRingCat} → ModuleCat ↑R → (AlgebraicGeometry.Spec R).Modules
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_one : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ↑1 = 1
-- Mathlib.Algebra.Order.Sub.Defs
/-- `OrderedSub α` means that `α` has a subtraction characterized by `a - b ≤ c ↔ a ≤ c + b`.
In other words, `a - b` is the least `c` such that `a ≤ b + c`.

This is satisfied both by the subtraction in additive ordered groups and by truncated subtraction
in canonically ordered monoids on many specific types.
 -/
OrderedSub : (α : Type u_2) → [LE α] → [Add α] → [Sub α] → Prop
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_id_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A.X A.X))
      CategoryTheory.AddMonObj.add
-- Mathlib.Data.Set.Function
Set.MapsTo.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁}
  {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂},
  Set.MapsTo f₁ s₁ t₁ → Set.MapsTo f₂ s₂ t₂ → Set.MapsTo (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- `DilationEquiv.toEquiv` as a monoid homomorphism.  -/
DilationEquiv.toPerm : {X : Type u_1} → [inst : PseudoEMetricSpace X] → (X ≃ᵈ X) →* Equiv.Perm X
-- Mathlib.FieldTheory.SeparableDegree
/-- If `α` is algebraic over `F`, then the separable degree of `F⟮α⟯ / F` is equal to the degree
of `F⟮α⟯ / F` if and only if `α` is a separable element.  -/
IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsAlgebraic F α → (Field.finSepDegree F ↥F⟮α⟯ = Module.finrank F ↥F⟮α⟯ ↔ IsSeparable F α)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.coimage.π f
-- Init.Data.SInt.Bitwise
Int64.toBitVec_xor : ∀ (a b : Int64), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Init.Internal.Order.Basic
Lean.Order.PProd.monotone_mk : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} [inst : Lean.Order.PartialOrder α] [inst_1 : Lean.Order.PartialOrder β]
  [inst_2 : Lean.Order.PartialOrder γ] {f : γ → α} {g : γ → β},
  Lean.Order.monotone f → Lean.Order.monotone g → Lean.Order.monotone fun x => ⟨f x, g x⟩
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ext_iff : ∀ {α : Type u_3} {inst : Preorder α} {x y : SuccOrder α}, x = y ↔ SuccOrder.succ = SuccOrder.succ
-- Init.Data.Int.Bitwise.Lemmas
_private.Init.Data.Int.Bitwise.Lemmas.0.Int.shiftRight.match_1.splitter : (motive : ℤ → ℕ → Sort u_1) →
  (x : ℤ) → (x_1 : ℕ) → ((n s : ℕ) → motive (Int.ofNat n) s) → ((n s : ℕ) → motive (Int.negSucc n) s) → motive x x_1
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.mk : Array (Lean.TSyntax `Lean.Parser.Term.funBinder) → Lean.DoSeq → Lean.Elab.Do.ForwardArg
-- Std.Http.Data.Method
/-- Remove a link relationship between resources.
Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.3
 -/
Std.Http.Method.unlink : Std.Http.Method
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.slash_one : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {inst : Monoid G} {inst_1 : AddMonoid α} [self : SlashAction β G α]
  (k : β) (a : α), SlashAction.map k 1 a = a
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.exists_isLUB : ∀ {s : Set ℝ}, s.Nonempty → BddAbove s → ∃ x, IsLUB s x
-- Init.Data.Rat.Lemmas
Rat.mkRat_add_mkRat : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℕ}, d₁ ≠ 0 → d₂ ≠ 0 → mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)