mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Actions
/-- A predicate for Actions that ensures that the pivot of a clause is always included in the clause.
In the LRAT format, the clause's pivot is always its first literal. However, from an interface
perspective, it is awkward to require that all `Clause` implementations preserve the ordering of
their literals. It is also awkward to have the pivot in the `addRat` action not included in the
clause itself, since then the pivot would need to be readded to the clause when it is added to the
formula. So to avoid imposing awkward constraints on the `Clause` interface, and to avoid requiring
`Formula` implementations to add pivots to the clauses provided by the `addRat` action, we use this
predicate to indicate that the pivot provided by the `addRat` action is indeed in the provided
clause.
 -/
Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction : {α : Type u_1} →
  {β : Type u_2} → [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → Std.Tactic.BVDecide.LRAT.Action β α → Prop
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn_zero : DyckWord.firstReturn 0 = 0
-- Mathlib.Algebra.GradedMonoid
SetLike.GradedMonoid.toGradedOne : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {inst : SetLike S R} {inst_1 : Monoid R} {inst_2 : AddMonoid ι}
  {A : ι → S} [self : SetLike.GradedMonoid A], SetLike.GradedOne A
-- Lean.Meta.Tactic.Grind.ForallProp
/-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions.  -/
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.mkEMatchTheoremWithKind'? : Lean.Meta.Grind.Origin →
  Lean.Expr →
    Lean.Meta.Grind.EMatchTheoremKind →
      Lean.Meta.Grind.SymbolPriorities → Lean.MetaM (Option Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s ∪ t₁ ⊆ s ∪ t₂
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LeftLift.IsAbsKan.hasAbsLeftKanLift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsAbsKan), CategoryTheory.Bicategory.HasAbsLeftKanLift f g
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_of_det_ne_zero : ∀ {m : Type um} {R : Type u_1} [inst : CommRing R] [IsDomain R] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {A : Matrix m m R}, A.det ≠ 0 → A.rank = Fintype.card m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey? k' =
    if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α fun x => β) (k : α)
  (h : (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).isSome = true),
  Std.DTreeMap.Internal.Impl.Const.getₘ l k h = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).get h
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  (x : C),
  ((CategoryTheory.Bicategory.Prod.sectR b C).mapId x).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mem_support_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {x : ℕ},
  x ∈ ((MvPolynomial.finSuccEquiv R n) f).support ↔ x ∈ (fun m => m 0) '' ↑f.support
-- Mathlib.Topology.EMetricSpace.Defs
/-- Given `f : β → ℝ≥0∞`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then closed `f i`-neighborhoods of the diagonal form a basis of `𝓤 α`.

For specific bases see `uniformity_basis_edist_le` and `uniformity_basis_edist_le'`.  -/
EMetric.mk_uniformity_basis_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal},
  (∀ (x : β), p x → 0 < f x) →
    (∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}
-- Mathlib.Condensed.Limits
instHasFiniteLimitsCondensed : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasFiniteLimits A],
  CategoryTheory.Limits.HasFiniteLimits (Condensed A)
-- Mathlib.Data.Seq.Computation
Computation.mem_of_promises : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] {a : α}, s.Promises a → a ∈ s
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t ∈ ∂⁺^k 𝒜` iff `t` is exactly `k` elements less than something in `𝒜`.

See also `Finset.mem_upShadow_iterate_iff_exists_sdiff`.  -/
Finset.mem_upShadow_iterate_iff_exists_mem_card_add : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + k
-- Mathlib.Topology.Closure
Dense.exists_mem_open : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → ∀ {U : Set X}, IsOpen U → U.Nonempty → ∃ x ∈ s, x ∈ U
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
ContMDiffVectorBundle.continuousLinearMap : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {n : WithTop ℕ∞} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B]
  [inst_18 : FiberBundle F₁ E₁] [inst_19 : VectorBundle 𝕜 F₁ E₁] [inst_20 : FiberBundle F₂ E₂]
  [inst_21 : VectorBundle 𝕜 F₂ E₂] [inst_22 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_23 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB],
  ContMDiffVectorBundle n (F₁ →L[𝕜] F₂) (fun b => E₁ b →L[𝕜] E₂ b) IB
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [F.PreservesFiniteEffectiveEpiFamilies], F.PreservesEffectiveEpis
-- Mathlib.GroupTheory.GroupAction.Defs
/-- When you take a set `U` in `α`, push it down to the quotient, and pull back, you get the union
of the orbit of `U` under `G`.  -/
AddAction.quotient_preimage_image_eq_union_add : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (U : Set α),
  Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x => g +ᵥ x) '' U
-- Mathlib.Algebra.Ring.Defs
/-- A not-necessarily-unital, not-necessarily-associative semiring. See `CommutatorRing` and the
documentation thereof in case you need a `NonUnitalNonAssocSemiring` instance on a Lie ring
or a Lie algebra.  -/
NonUnitalNonAssocSemiring : Type u → Type u
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The setoid of splittings with `N`-conjugacy  -/
GroupExtension.IsConj.setoid : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] → {E : Type u_3} → [inst_2 : Group E] → (S : GroupExtension N E G) → Setoid S.Splitting
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_union_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- Given a Lie-Rinehart algebra `L` containing a LieRinehart subalgebra `L' ⊆ L`, together with a
Lie ring module `M` of `L`, we may regard `M` as a Lie ring module of `L'` by restriction.  -/
LieRinehartSubalgebra.lieRingModule : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          (L' : LieRinehartSubalgebra A L) →
            {M : Type u_3} → [inst_3 : AddCommGroup M] → [LieRingModule L M] → LieRingModule (↥L') M
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_zero_basis : (nhds 0).HasBasis (fun a => 0 < a) fun a => Set.Iio a
-- Init.Data.String.PosRaw
String.getUTF8Byte_eq_getElem : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos}, s.getUTF8Byte p h = s.toByteArray[p.byteIdx]
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.sigmaFinite_of_countable : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable → (∀ s ∈ S, μ s < ⊤) → ⋃₀ S = Set.univ → MeasureTheory.SigmaFinite μ
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `proj i j` is the quadratic map sending the vector `x : n → R` to `x i * x j`  -/
QuadraticMap.proj : {R : Type u_3} →
  {A : Type u_7} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [SMulCommClass R A A] → [IsScalarTower R A A] → {n : Type u_9} → n → n → QuadraticMap R (n → A) A
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below : {ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} →
        {a : s.Pos} →
          {motive : (a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1 → Prop} →
            {a_1 : s.Pos} → String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1 → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_sub_le : ∀ {G : Type u_1} [inst : AddGroup G] {s t : Set G}, Nat.card ↑(s - t) ≤ Nat.card ↑s * Nat.card ↑t
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.Subobject.ofMkLEMk f f ⋯ = CategoryTheory.CategoryStruct.id A₁
-- Mathlib.Data.Fintype.EquivFin
Fintype.exists_ne_of_one_lt_card : ∀ {α : Type u_1} [inst : Fintype α], 1 < Fintype.card α → ∀ (a : α), ∃ b, b ≠ a
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_rci : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo (Std.Slice.toList xs)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The binary product in the category of a `SemilatticeInf` with `OrderTop` is the same as the
infimum.
 -/
CategoryTheory.Limits.CompleteLattice.prod_eq_inf : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (x y : α), (x ⨯ y) = x ⊓ y
-- Mathlib.Order.Bounds.Defs
IsCofinal.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsCofinal s = ∀ (x : α), ∃ y ∈ s, x ≤ y
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- A `StrongFEPair` structure with `f = oddKernel a` and `g = sinKernel a`.  -/
HurwitzZeta.hurwitzOddFEPair : UnitAddCircle → WeakFEPair ℂ
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_map_eq_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).natDegree = p.natDegree
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_eq_false_iff : ∀ {s : String}, s.isEmpty = false ↔ s ≠ ""
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.compRight_apply : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabeling K} (f : K → K')
  (e : ↑G.edgeSet), C.compRight f e = f (C e)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift_comp_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))),
  (Monoid.Coprod.clift f hM₁ hN₁ hM hN).comp Monoid.Coprod.mk = f
-- Lean.Parser.Term
Lean.Parser.Term.letConfig.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f y` over `y ∈ g '' s` equals the product of `f (g i)` over `s`
provided that `g` is injective on `s ∩ mulSupport (f ∘ g)`.  -/
finprod_mem_image' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set β} {g : β → α},
  Set.InjOn g (s ∩ Function.mulSupport (f ∘ g)) → ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.measurable_uncurry_of_continuous_of_measurable : ∀ {α : Type u_5} {β : Type u_6} {ι : Type u_7} [inst : TopologicalSpace ι] [TopologicalSpace.MetrizableSpace ι]
  [inst_2 : MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] {mβ : MeasurableSpace β}
  [inst_5 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {m : MeasurableSpace α}
  {u : ι → α → β},
  (∀ (x : α), Continuous fun i => u i x) → (∀ (i : ι), Measurable (u i)) → Measurable (Function.uncurry u)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.ofSurjective_σ : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Type w}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective ⇑f) (x : S),
  (Algebra.Extension.ofSurjective f h).σ x = ⋯.choose
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : γ k},
      Std.Internal.List.getValueCastD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback =
        (Option.map (f k) (Std.Internal.List.getValueCast? k l)).getD fallback
-- Init.Omega.LinearCombo
Lean.Omega.instDecidableEqLinearCombo.decEq : (x x_1 : Lean.Omega.LinearCombo) → Decidable (x = x_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.himp : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α}, MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ ⇨ s₂)
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.find_apply_of_mem : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)},
  IsChain (fun x1 x2 => x1 ≤ x2) c →
    ∀ (ne : c.Nonempty) {i : ι} {v : ShrinkingLemma.PartialRefinement u s p},
      v ∈ c → i ∈ v.carrier → (ShrinkingLemma.PartialRefinement.find c ne i).toFun i = v.toFun i
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.Limits.pullback.snd f I.subschemeι) =
    (I.comap f).subschemeMap I f ⋯
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_eq_top_iff_subset : ∀ {M : Type u_1} {S : Set M} [inst : AddSemigroup M], S.addCentralizer = Set.univ ↔ S ⊆ Set.addCenter M
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t → t.get! k = k
-- Mathlib.Data.TwoPointing
/-- The sum of two pointings. Keeps the first point from the left and the second point from the
right.  -/
TwoPointing.sum : {α : Type u_1} → {β : Type u_2} → TwoPointing α → TwoPointing β → TwoPointing (α ⊕ β)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv_right₀`. -/
AntivaryOn.of_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < g i) → AntivaryOn f g⁻¹ s → MonovaryOn f g s
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w')
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y],
  CategoryTheory.Localization.HasSmallLocalizedHom W X Y
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_zero : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M},
  ↑0 = 0
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.isPredLimit_of_not_isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsPredPrelimit a → ¬IsMax a → Order.IsPredLimit a
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The restriction of an algebra norm to a subalgebra.  -/
AlgebraNorm.restriction : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} →
      [inst_1 : Ring S] → [inst_2 : Algebra R S] → (A : Subalgebra R S) → AlgebraNorm R S → AlgebraNorm R ↥A
-- Lean.ProjFns
Lean.Environment.getAuxParentProjectionInfo? : Lean.Environment → Lean.Name → Option Lean.AuxParentProjectionInfo
-- Std.Http.Protocol.H1
/-- Replaces only the reader state variant (`needHeader`, `readBody`, `failed`, ...)
without touching buffered input or parsed message metadata.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.setReaderState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Reader.State dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instPartialOrder : {R : Type u} → {M : Type v} → [inst : VAdd R M] → PartialOrder (SubAddAction R M)
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_nonneg : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A), 0 ≤ p.supNorm
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.token.inj : ∀ {val val_1 : Lean.Parser.Token},
  Lean.Parser.ParserExtension.OLeanEntry.token val = Lean.Parser.ParserExtension.OLeanEntry.token val_1 → val = val_1
-- Mathlib.Algebra.Opposites
/-- The element of `PreOpposite α` that represents `x : α`.  -/
PreOpposite.op' : {α : Type u_3} → α → PreOpposite α
-- Init.Data.String.Basic
String.data_injective : ∀ {s₁ s₂ : String}, s₁.toList = s₂.toList → s₁ = s₂
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_bot : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (a : M), a • ⊥ = ⊥
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSubtype.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : { a // P a } → Sort u_2) (v : α) (property : P v)
  (h_1 : (v : α) → (property : P v) → motive ⟨v, property⟩),
  (match ⟨v, property⟩ with
    | ⟨v, property⟩ => h_1 v property) =
    h_1 v property
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
/-- `A` is in row echelon form and `l i` is the leading position of each row `i`,
with `⊤` for a zero row.  -/
Matrix.IsPivotedBy : {m : Type u_1} → {n : Type u_2} → {R : Type u_3} → [Zero R] → [LT m] → [LT n] → Matrix m n R → (m → WithTop n) → Prop
-- Lean.Meta.Match.MatcherApp.Transform
/-- Overlap parameter fvars (non-casesOn splitters only).  -/
Lean.Meta.MatcherApp.TransformAltFVars.overlaps : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_inl : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β], IsUniformEmbedding Sum.inl
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Data.List.SplitBy
List.splitBy.loop.eq_1 : ∀ {α : Type u} (R : α → α → Bool) (a : α) (a_1 : List α) (a_2 : List (List α)) (a_3 : α) (as : List α),
  List.splitBy.loop R (a_3 :: as) a a_1 a_2 =
    match R a a_3 with
    | true => List.splitBy.loop R as a_3 (a :: a_1) a_2
    | false => List.splitBy.loop R as a_3 [] ((a :: a_1).reverse :: a_2)
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_aux4 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  ↑p ^ (n + 1) * WittVector.wittMul p (n + 1) =
    -(↑p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (↑p ^ (n + 1) * MvPolynomial.X (1, n + 1)) +
          ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      (WittVector.remainder p n - WittVector.wittPolyProdRemainder p (n + 1))
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.IsColimit.isIso_colimMap_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [inst_2 : CategoryTheory.IsConnected J] {F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasColimit F]
  {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsIso (CategoryTheory.Limits.colimMap c.ι)
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Returns `true` if `e` is a `Grind.MatchCond`, and it has been satisfied.
Recall that we use `Grind.MatchCond` to annotate conditional `match`-equations.
Consider the following example:
```
inductive S where
  | mk1 (n : Nat)
  | mk2 (n : Nat) (s : S)
  | mk3 (n : Bool)
  | mk4 (s1 s2 : S)

def f (x y : S) :=
  match x, y with
  | .mk1 _, _ => 2
  | _, .mk2 1 (.mk4 _ _) => 3
  | .mk3 _, _ => 4
  | _, _ => 5
```
The `match`-expression in the example above has overlapping patterns and
consequently produces conditional `match` equations. Thus, `grind` generates
the following auxiliary `Grind.MatchCond` terms for an application `f a b`:
- `Grind.MatchCond (∀ (n : Nat), a = S.mk1 n → False)`
- `Grind.MatchCond (∀ (s1 s2 : S), b = S.mk2 1 (s1.mk4 s2) → False)`
- `Grind.MatchCond (∀ (n : Bool), a = S.mk3 n → False)`

`isSatisfied` uses the fact that constructor applications and literal values
are always the root of their equivalence classes.
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.isSatisfied : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The **binomial inverse theorem** (variant of the Woodbury identity).  -/
Matrix.add_mul_mul_inv_eq_sub' : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α)
  (V : Matrix m n α),
  IsUnit A →
    IsUnit (C + C * V * A⁻¹ * U * C) → (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹