mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.exists_ne : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ∀ (z : α), ∃ x ∈ s, x ≠ z
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.unique : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y y' : F},
  BoxIntegral.HasIntegral I l f vol y → BoxIntegral.HasIntegral I l f vol y' → y = y'
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.IsAssociatedPrime.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R}, I.IsPrime → (∃ x, I = (N.colon {x}).radical) → N.IsAssociatedPrime I
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_finVal : ∀ (n : Fin UInt64.size), UInt64.ofNatLT ↑n ⋯ = UInt64.ofFin n
-- Init.Data.Vector.Attach
Vector.reverse_attachWith : ∀ {α : Type u_1} {n : ℕ} {P : α → Prop} {xs : Vector α n} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The tautological action by `M₁ →L[R₁] M₁` on `M`.

This generalizes `Function.End.applyMulAction`.  -/
ContinuousLinearMap.applyModule : {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₁] → Module (M₁ →L[R₁] M₁) M₁
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv_eq_iff : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (a : ↥S.leftInv) (b : M), ↑(S.fromLeftInv a) = b ↔ ↑a * b = 1
-- Init.Data.Bool
Bool.and_eq_left_iff_imp : ∀ {a b : Bool}, (a && b) = a ↔ a = true → b = true
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- If `e.fixedReduce` is not a homothety, then there are a linear form `f` and
a vector `v` such that `f` vanishes on `e.fixedSubmodule ⊔ K ∙ (e v - v)`, `f v = 1`,
and the images of `v` and `e v` in `V ⧸ e.fixedSubmodule` are linearly independent.  -/
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.exists_dual_of_fixedReduce_ne_smul : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] {e : V ≃ₗ[K] V},
  (∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x) →
    1 < Module.finrank K (V ⧸ (↑e).fixedSubmodule) →
      ∃ f v,
        LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
          (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ LinearMap.ker f ∧ f v = 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The morphism `H ⟶ A` induced by a morphism `k : K ⟶ A` such that `f' ≫ k = 0`  -/
CategoryTheory.ShortComplex.LeftHomologyData.descH : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → {A : C} → (k : h.K ⟶ A) → CategoryTheory.CategoryStruct.comp h.f' k = 0 → (h.H ⟶ A)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminormClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} [inst : AddGroup α] [inst_1 : FunLike F α ℝ]
  [toNonarchimedeanHomClass : NonarchimedeanHomClass F α ℝ],
  (∀ (f : F), f 0 = 0) → (∀ (f : F) (a : α), f (-a) = f a) → NonarchAddGroupSeminormClass F α
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_iff_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, Order.succ a ≤ a ↔ IsMax a
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₂.HasTensor X₃]
  [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.Tactic.Linter.GlobalAttributeIn
/-- `getGlobalAttributesIn? cmd` assumes that `cmd` represents a `attribute [...] id in ...` command.
If this is the case, then it returns `(id, #[non-local nor scoped attributes])`.
Otherwise, it returns `default`.
 -/
_private.Mathlib.Tactic.Linter.GlobalAttributeIn.0.Mathlib.Linter.globalAttributeInLinter.getGlobalAttributesIn? : Lean.Syntax → Option (Lean.Ident × Array (Lean.TSyntax `attr))
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the composition.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.right₀_nth : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (n : ℕ), T.right₀.nth n = T.nth ↑n
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.exists_minimalPrimes_le : ∀ {R : Type u_1} [inst : CommSemiring R] {I J : Ideal R} [J.IsPrime], I ≤ J → ∃ p ∈ I.minimalPrimes, p ≤ J
-- Mathlib.RingTheory.Localization.Defs
/-- `IsLocalization.mk' S` is the surjection sending `(x, y) : R × M` to
`f x * (f y)⁻¹`.  -/
IsLocalization.mk' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Submonoid R} →
      (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → R → ↥M → S
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- A tagged prepartition is a prepartition enriched with a tagged point for each box of the
prepartition. For simplicity we require that `tag` is defined for all boxes in `ι → ℝ` but
we will use only the values of `tag` on the boxes of the partition.  -/
BoxIntegral.TaggedPrepartition : {ι : Type u_1} → BoxIntegral.Box ι → Type u_1
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.div_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x / g x) l (nhds 0)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- The interior of a box.  -/
BoxIntegral.Box.Ioo : {ι : Type u_1} → BoxIntegral.Box ι →o Set (ι → ℝ)
-- Init.Data.Option.Attach
Option.unattach_guard : ∀ {α : Type u_1} {p : α → Prop} {q : { x // p x } → Bool} {r : α → Bool},
  (∀ (x : α) (h : p x), q ⟨x, h⟩ = r x) → ∀ {x : { x // p x }}, (Option.guard q x).unattach = Option.guard r ↑x
-- Mathlib.Data.Set.Image
Set.Quotient.range_mk'' : ∀ {α : Type u_1} {sa : Setoid α}, Set.range Quotient.mk'' = Set.univ
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_le : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] (a b : WithZero (Multiplicative α)),
  WithZero.toMulBot a ≤ WithZero.toMulBot b ↔ a ≤ b
-- Lean.Environment
Lean.instReprConstantKind : Repr Lean.ConstantKind
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.integral_toReal_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_inverseImage_iff : ∀ {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] (J : Type u') [inst_2 : CategoryTheory.Category.{v', u'} J]
  (P : CategoryTheory.ObjectProperty D) [P.IsClosedUnderIsomorphisms] (e : C ≌ D),
  (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w},
  (x.sshiftRight' y).toNat = if x.msb = true then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat else x.toNat >>> y.toNat
-- Mathlib.CategoryTheory.Pi.Basic
/-- Pull back an `I`-indexed family of objects to a `J`-indexed family, along a function `J → I`.
 -/
CategoryTheory.Pi.comap : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₁} → (h : J → I) → CategoryTheory.Functor ((i : I) → C i) ((j : J) → C (h j))
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g k c : Equiv.Perm α},
  k ∈ Subgroup.centralizer {g} → c ∈ g.cycleFactorsFinset → ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_eraseₘaux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.eraseₘaux a)).buckets).Perm
      (Std.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafify_sheafifyLift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyLift J η hQ) = η
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_empty : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.size = 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.DTreeMap.Raw.isEmpty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Bool
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_apply' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E),
      ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ =
        ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ
-- Std.Data.ExtTreeSet.Basic
/-- Returns the `n`-th smallest element, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtTreeSet.atIdxD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → ℕ → α → α
-- Mathlib.Tactic.Contrapose
/-- `contrapose` transforms the main goal into its contrapositive. If the goal has the form `⊢ P → Q`,
then `contrapose` turns it into `⊢ ¬ Q → ¬ P`. If the goal has the form `⊢ P ↔ Q`, then `contrapose`
turns it into `⊢ ¬ P ↔ ¬ Q`.

* `contrapose h` on a goal of the form `h : P ⊢ Q` turns the goal into `h : ¬ Q ⊢ ¬ P`. This is
  equivalent to `revert h; contrapose; intro h`.
* `contrapose h with new_h` uses the name `new_h` for the introduced hypothesis. This is equivalent
  to `revert h; contrapose; intro new_h`.
* `contrapose!`, `contrapose! h` and `contrapose! h with new_h` push negation deeper into the goal
  after contraposing (but before introducing the new hypothesis). See the `push Not` tactic for more
  details on the pushing algorithm.
* `contrapose! (config := cfg)` controls the options for negation pushing. All options for
  `Mathlib.Tactic.Push.Config` are supported:
  * `contrapose! +distrib` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` instead of `p → ¬ q`.

Examples:
```lean4
variables (P Q R : Prop)

example (H : ¬ Q → ¬ P) : P → Q := by
  contrapose
  exact H

example (H : ¬ P ↔ ¬ Q) : P ↔ Q := by
  contrapose
  exact H

example (H : ¬ Q → ¬ P) (h : P) : Q := by
  contrapose h
  exact H h

example (H : ¬ R → P → ¬ Q) : (P ∧ Q) → R := by
  contrapose!
  exact H

example (H : ¬ R → ¬ P ∨ ¬ Q) : (P ∧ Q) → R := by
  contrapose! +distrib
  exact H
```
 -/
Mathlib.Tactic.Contrapose.contrapose : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Orbits of an element form a partition  -/
MulAction.IsPartition.of_orbits : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X],
  Setoid.IsPartition (Set.range fun a => MulAction.orbit G a)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- The linear equivalence that maps a continuous linear map to the type copy endowed with the
uniform convergence topology.  -/
ContinuousLinearMap.toUniformConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] →
                              (𝔖 : Set (Set E)) → (E →SL[σ] F) ≃ₗ[𝕜₂] UniformConvergenceCLM σ F 𝔖
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.uIcc_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α},
  s.OrdConnected → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
-- Mathlib.Order.Partition.Equipartition
/-- There exists an enumeration of an equipartition's parts where
larger parts map to smaller numbers and vice versa.  -/
Finpartition.IsEquipartition.exists_partsEquiv : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → ∃ f, ∀ (t : ↥P.parts), (↑t).card = s.card / P.parts.card + 1 ↔ ↑(f t) < s.card % P.parts.card
-- Mathlib.SetTheory.Ordinal.Basic
/-- The cardinal of an ordinal is the cardinality of any type on which a relation with that order
type is defined.  -/
Ordinal.card : Ordinal.{u_1} → Cardinal.{u_1}
-- Init.Data.Order.Lemmas
Std.instTotalLeOfIsLinearPreorder : ∀ {α : Type u} [inst : LE α] [Std.IsLinearPreorder α], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Iio : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α} [NoMinOrder α], IsConnected (Set.Iio a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Evaluation at a point as an affine map.  -/
AffineMap.proj : {k : Type u_1} →
  [inst : Ring k] →
    {ι : Type u_10} →
      {V : ι → Type u_11} →
        {P : ι → Type u_12} →
          [inst_1 : (i : ι) → AddCommGroup (V i)] →
            [inst_2 : (i : ι) → Module k (V i)] →
              [inst_3 : (i : ι) → AddTorsor (V i) (P i)] → (i : ι) → ((i : ι) → P i) →ᵃ[k] P i
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_conj : ∀ (z τ : ℂ), (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.toFreeAddGroup_symm_apply : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] (a : FreeAddGroup (IsFreeAddGroup.Generators G)),
  (IsFreeAddGroup.toFreeAddGroup G).symm a = (IsFreeAddGroup.addEquiv G) a
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The quotient of a Noetherian ring of krull dimension less than or equal to `1` by a principal ideal
is of finite length.
 -/
isFiniteLength_quotient_span_singleton : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {x : R},
  x ∈ nonZeroDivisors R → IsFiniteLength R (R ⧸ Ideal.span {x})
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.«tactic_clause(Add_)» : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_biSup : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Type u_1} {I : Set ι},
  I.Finite → ∀ {f : ι → Filter α}, (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded
-- Mathlib.Tactic.Positivity.Basic
/-- **Alias** of the reverse direction of `Rat.num_nonneg`. -/
Mathlib.Meta.Positivity.num_nonneg_of_nonneg : ∀ {q : ℚ}, 0 ≤ q → 0 ≤ q.num
-- Mathlib.Analysis.Calculus.Deriv.Shift
derivWithin_comp_neg : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (-x)) s x = -derivWithin f (-s) (-x)
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.IsWeak.continuous_iff : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] {α : Type u_7} [inst_7 : TopologicalSpace α]
  {f : α → E}, Continuous f ↔ ∀ (y : F), Continuous fun x => (B (f x)) y
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιNatTrans_app_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C}
  (f : X ⟶ Y) (d : ↑(F.obj X)),
  ((CategoryTheory.Grothendieck.ιNatTrans f).app d).fiber =
    CategoryTheory.CategoryStruct.id ((F.map f).toFunctor.obj ((CategoryTheory.Grothendieck.ι F X).obj d).fiber)
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.equiv_image_eq_iff_subset : ∀ {α : Type u_1} {s : Set α} (e : α ≃ α), s.Finite → (⇑e '' s = s ↔ ⇑e '' s ⊆ s)
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.num.sizeOf_spec : ∀ (k : ℕ), sizeOf (Lean.Meta.Sym.Offset.num k) = 1 + sizeOf k
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.dandThen : Lean.Meta.Simp.DSimproc → Lean.Meta.Simp.DSimproc → Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- See `LinearIndependent.finSnoc` for a family of elements in a vector space.  -/
LinearIndependent.finSnoc' : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : ℕ} (v : Fin m → M)
  (x : M),
  LinearIndependent R v →
    (∀ (c : R), ∀ y ∈ Submodule.span R (Set.range v), c • x + y = 0 → c = 0) → LinearIndependent R (Fin.snoc v x)
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.inverse_map_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  {X Y : CategoryTheory.Functor (CategoryTheory.SingleObj G) V} (f : X ⟶ Y),
  (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.edits : Lean.Lsp.TextDocumentEdit → Lean.Lsp.TextEditBatch
-- Mathlib.Topology.MetricSpace.HausdorffDimension
AntilipschitzWith.le_dimH_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
  AntilipschitzWith K f → ∀ (s : Set X), dimH s ≤ dimH (f '' s)
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- The left unitors are given by equalities  -/
CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_6 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.udiv with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_6 ()
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_apply_support_val : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (a : ↥(Finsupp.supported M R s)),
  ((Finsupp.supportedEquivFinsupp s) a).support.val =
    Multiset.map (fun x => ⟨↑x, ⋯⟩) (Multiset.filter (fun x => x ∈ s) (↑a).support.val).attach
-- Lean.Meta.ForEachExpr
_private.Lean.Meta.ForEachExpr.0.Lean.Meta.visitLambda.visit : {m : Type → Type u_1} →
  [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Array Lean.Expr → Lean.Expr → m Unit
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Inhabited α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → l.minKey! = Std.Internal.List.minKey! l.toListModel
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f],
  IsLocalizedModule.fromLocalizedModule S f =
    { toFun := IsLocalizedModule.fromLocalizedModule' S f, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurentAlg_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R), Polynomial.toLaurentAlg f = Polynomial.toLaurent f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.mk.inj : ∀ {used : Lean.PHashSet Lean.Name} {next : Lean.PHashMap Lean.Name ℕ} {used_1 : Lean.PHashSet Lean.Name}
  {next_1 : Lean.PHashMap Lean.Name ℕ},
  { used := used, next := next } = { used := used_1, next := next_1 } → used = used_1 ∧ next = next_1
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- If `f` is a symmetric bilinear map taking values in the space of alternating maps,
then the twice uncurried `f` is zero.

See also `alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply`
for a formula that does not assume `f` to be symmetric.  -/
AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} {f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N},
  (∀ (x y : M), (f x) y = (f y) x) →
    AlternatingMap.alternatizeUncurryFin (AlternatingMap.alternatizeUncurryFinLM ∘ₗ f) = 0
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of `CompleteLattice.ofProp` on a function lattice.  -/
Lean.Order.CompleteLattice.ofProp_apply : ∀ {σ : Type v} {β : Type u} [inst : Lean.Order.CompleteLattice β] (p : Prop) (s : σ),
  Lean.Order.CompleteLattice.ofProp p s = Lean.Order.CompleteLattice.ofProp p