mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SymmDiff
bihimp_right_involutive : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), Function.Involutive fun x => bihimp a x
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₗ D) (X : D ⥤ₗ E),
  (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_getLast?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max? = t.toList.getLast?
-- Mathlib.Data.List.Basic
List.exists_mem_cons_iff : ∀ {α : Type u} (p : α → Prop) (a : α) (l : List α), (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.EffectivePresentation.mk : {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] →
        {F : CategoryTheory.Functor C D} →
          {X : D} → (p : C) → (f : F.obj p ⟶ X) → CategoryTheory.EffectiveEpi f → F.EffectivePresentation X
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight_comp : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V}
  (p : Quiver.Path a b) (q : Quiver.Path b c),
  Quiver.Path.addWeight (fun {i j} => w) (p.comp q) =
    Quiver.Path.addWeight (fun {i j} => w) p + Quiver.Path.addWeight (fun {i j} => w) q
-- Mathlib.Algebra.CharZero.Quotient
QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {p : R} {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ},
  n ≠ 0 → (n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n))
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_sInter : ∀ {α : Type u_2} [inst : Bornology α] {S : Set (Set α)},
  S.Finite → (Bornology.IsCobounded (⋂₀ S) ↔ ∀ s ∈ S, Bornology.IsCobounded s)
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain of a `LatticeHom`.  -/
LatticeHom.withTop' : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → [OrderTop β] → LatticeHom α β → LatticeHom (WithTop α) β
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom_id : ∀ {R : Type u} [inst : CommSemiring R], CommRing.Pic.mapRingHom (RingHom.id R) = MonoidHom.id (CommRing.Pic R)
-- Batteries.Data.List.Basic
/-- Auxiliary for `takeWhile₂TR`:
`takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ as', acca.reverse ++ bs')`
if `takeWhile₂ R as bs = (as', bs')`.  -/
List.takeWhile₂TR.go : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → List α → List β → List α → List β → List α × List β
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.max ⋯)).isLE = true
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_equivUnitsAffineMap_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ),
  (AffineEquiv.equivUnitsAffineMap.symm u).linear =
    (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- Auxiliary sequence for the proof that `smoothingFun` is nonarchimedean.  -/
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu : {R : Type u_1} →
  [inst : CommRing R] →
    (μ : RingSeminorm R) →
      {x y : R} →
        (∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)) → ℕ → ℕ
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Replace the `m`-th coefficient of an element `x` of the monoid algebra by a given value `r : R`.
If `r = 0`, this is equal to `x.erase m`.  -/
AddMonoidAlgebra.update : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R → AddMonoidAlgebra R M → AddMonoidAlgebra R M
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_insert_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] {g : N →ₙ+ P}
  {f₁ f₂ : M →ₙ+ N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.foldM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (init : δ) (b : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.foldM f init b =
    Array.foldlM (fun acc l => Std.DHashMap.Internal.AssocList.foldlM f acc l) init b.buckets
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mk.injEq : ∀ {α : Type u_1} [inst : CompleteLattice α] (toSublattice : Sublattice α)
  (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier)
  (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier)
  (toSublattice_1 : Sublattice α)
  (sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier)
  (sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier),
  ({ toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' } =
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 }) =
    (toSublattice = toSublattice_1)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.id_pair : {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.pair i j)
-- Init.Data.Int.Bitwise.Lemmas
Int.zero_shiftRight : ∀ (n : ℕ), 0 >>> n = 0
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extend.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition n), c.extend none = c.extendLeft
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [s.OrdConnected] (a b : ↑s),
  Subtype.val '' Set.uIoc a b = Set.uIoc ↑a ↑b
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.mk : {P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      [toNondegenerate : Configuration.Nondegenerate P L] →
        (mkPoint : {l₁ l₂ : L} → l₁ ≠ l₂ → P) →
          (∀ {l₁ l₂ : L} (h : l₁ ≠ l₂), mkPoint h ∈ l₁ ∧ mkPoint h ∈ l₂) → Configuration.HasPoints P L
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is greater than its mean on a set of positive
measure.  -/
MeasureTheory.measure_setAverage_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_intCast_mul : ∀ {R : Type u} [inst : Ring R] {n : ℤ} {f : Polynomial R}, Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.updateRuleSet : Aesop.LocalRuleSet → Aesop.Frontend.TacticConfig → Lean.MVarId → Lean.Elab.TermElabM Aesop.LocalRuleSet
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addZ_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  WeierstrassCurve.Jacobian.addZ P (W'.neg P) = 0
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.addHom_ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass β] {f g : Multiset α →+ β}, f = g ↔ ∀ (x : α), f {x} = g {x}
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i))
        h)
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), LowerSet.Iic a = { carrier := Set.Iic a, lower' := ⋯ }
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorem.mk.inj : ∀ {funPropName : Lean.Name} {thmOrigin funOrigin : Mathlib.Meta.FunProp.Origin} {mainArgs : Array ℕ}
  {appliedArgs priority : ℕ} {form : Mathlib.Meta.FunProp.TheoremForm} {funPropName_1 : Lean.Name}
  {thmOrigin_1 funOrigin_1 : Mathlib.Meta.FunProp.Origin} {mainArgs_1 : Array ℕ} {appliedArgs_1 priority_1 : ℕ}
  {form_1 : Mathlib.Meta.FunProp.TheoremForm},
  { funPropName := funPropName, thmOrigin := thmOrigin, funOrigin := funOrigin, mainArgs := mainArgs,
        appliedArgs := appliedArgs, priority := priority, form := form } =
      { funPropName := funPropName_1, thmOrigin := thmOrigin_1, funOrigin := funOrigin_1, mainArgs := mainArgs_1,
        appliedArgs := appliedArgs_1, priority := priority_1, form := form_1 } →
    funPropName = funPropName_1 ∧
      thmOrigin = thmOrigin_1 ∧
        funOrigin = funOrigin_1 ∧
          mainArgs = mainArgs_1 ∧ appliedArgs = appliedArgs_1 ∧ priority = priority_1 ∧ form = form_1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.consEquiv_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : α 0 × ((i : Fin n) → α i.succ)) (i : Fin (n + 1)),
  (Fin.consEquiv α) f i = Fin.cons f.1 f.2 i
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (n : N),
  SemidirectProduct.rightHom (SemidirectProduct.inl n) = 1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_add : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (D1 D2 : Derivation R A M), ⇑(D1 + D2) = ⇑D1 + ⇑D2
-- Mathlib.Order.PartialSups
disjoint_partialSups_right : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : DistribLattice α]
  [inst_3 : OrderBot α] {f : ι → α} {i : ι} {x : α}, Disjoint x ((partialSups f) i) ↔ ∀ j ≤ i, Disjoint x (f j)
-- Mathlib.Algebra.Category.Grp.Adjunctions
MonCat.val_inv_units_map_hom_apply : ∀ {X Y : MonCat} (f : X ⟶ Y) (u : (↑X)ˣ), ↑((GrpCat.Hom.hom (MonCat.units.map f)) u)⁻¹ = (MonCat.Hom.hom f) ↑u⁻¹
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function is less than another is Diophantine.  -/
Dioph.lt_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v < g v}
-- Mathlib.Analysis.Complex.Norm
Complex.norm_neg' : ∀ (z : ℂ), ‖-z‖ = ‖z‖
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.empty : ∀ {M : Type u_1} [inst : AddCommMonoid M], IsProperSemilinearSet ∅
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.addSemiconjBy_iff : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {x y z : (i : I) → f i},
  AddSemiconjBy x y z ↔ ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_zero_sub_comm : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
-- Mathlib.Data.Set.Image
Set.range_singleton : ∀ {α : Type u_1} {β : Type u_2} {x : α} (f : ↑{x} → β), Set.range f = {f ⟨x, ⋯⟩}
-- Init.Data.SInt.Lemmas
ISize.not_lt_minValue : ∀ {a : ISize}, ¬a < ISize.minValue
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''},
  MDiffAt g (f x) →
    MDiffAt f x → ∀ (v : TangentSpace I x), (mfderiv% (g ∘ f) x) v = (mfderiv% g (f x)) ((mfderiv% f x) v)
-- Init.PropLemmas
forall₄_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop},
  (∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d) →
    ((∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) ↔
      ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.subsingleton_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], Subsingleton ↥⊥
-- Mathlib.Data.Sym.Basic
/-- Another definition of the nth symmetric power, using vectors modulo permutations. (See `Sym`.)
 -/
Sym.Sym' : Type u_3 → ℕ → Type u_3
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.lTensor_bijective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑f
-- Mathlib.Computability.NFA
NFA.mk.sizeOf_spec : ∀ {α : Type u} {σ : Type v} [inst : SizeOf α] [inst_1 : SizeOf σ] (step : σ → α → Set σ) (start accept : Set σ),
  sizeOf { step := step, start := start, accept := accept } = 1
-- Mathlib.RepresentationTheory.Equiv
Representation.freeLift_single_single : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) {α : Type w'} (i : α) (g : G) (r : k) (f : α → V),
  ((σ.freeLift f) fun₀ | i => MonoidAlgebra.single g r) = r • (σ g) (f i)
-- Mathlib.Data.Prod.Basic
Prod.instIrreflLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl r] [Std.Irrefl s],
  Std.Irrefl (Prod.Lex r s)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring contains the ring's 0.  -/
Subring.zero_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), 0 ∈ s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The map `orderMonoidIso v` is strictly monotone.  -/
ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible], StrictMono ⇑(ValuativeRel.ValueGroupWithZero.orderMonoidIso v)
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instTopologicalSpace.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  DomMulAct.instTopologicalSpace = TopologicalSpace.induced (⇑DomMulAct.mk.symm) inst
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldl.eq_def : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ) (x_1 : RBTree.RBNode α),
  RBTree.RBNode.foldl f x x_1 =
    match x, x_1 with
    | b, RBTree.RBNode.nil => b
    | b, RBTree.RBNode.node c l v r => RBTree.RBNode.foldl f (f (RBTree.RBNode.foldl f b l) v) r
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_h' : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) (i : ι), b.symm.h' i = -b.h' i
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_insert_of_symm_of_notMem : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  a ∉ s → ((insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.adjunctionOfEquivRight_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
  (he :
    ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
      (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g))
  (Y : D),
  (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).counit.app Y =
    (e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.inv_le_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, a⁻¹ ≤ 1 ↔ 1 ≤ a
-- Init.Data.Slice.InternalLemmas
_private.Init.Data.Slice.InternalLemmas.0.Std.Slice.Internal.iter.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] (s : Std.Slice γ),
  Std.Slice.Internal.iter s = Std.ToIterator.iter s
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are finite extensions of `F`, with `A/F` Galois, such that `A ⊓ B = F`, then
`A` and `B` are linearly disjoint over `F`.
 -/
IntermediateField.LinearDisjoint.of_inf_eq_bot : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [IsGalois F ↥A] [FiniteDimensional F ↥A] [FiniteDimensional F ↥B], A ⊓ B = ⊥ → A.LinearDisjoint ↥B
-- Lean.Meta.Match.Match
Lean.Meta.Match.bootstrap.genMatcherCode : Lean.Option Bool
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.le_iff : ∀ {α : Type u_1} {f g : Filter α} (F : f.Realizer) (G : g.Realizer), f ≤ g ↔ ∀ (b : G.σ), ∃ a, F.F.f a ⊆ G.F.f b
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withAlts.mkSplitterHyps : Option Lean.Meta.Match.Overlaps → ℕ → Lean.Meta.Match.AltLHS → Array Lean.Expr → Lean.MetaM (Array Lean.Expr × Array ℕ)
-- Mathlib.Data.Bool.Basic
Bool.decide_true : ∀ {p : Prop} [inst : Decidable p], p → decide p = true
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.head_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B ⟶ X)
  (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows)
      (CategoryTheory.Limits.WidePushout.desc f fs w) =
    f
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n]
  [inst_2 : Fintype m] (M : Matrix l m R) (N : Matrix m n R), (M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey? =
        some (t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k')
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.isConnected_iff_nonempty_unique : ∀ (X : SSet), X.IsConnected ↔ Nonempty (Unique X.π₀)
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.inter : ∀ {α : Type u_2} {s t : Set α} [inst : LE α], CountableSupClosed s → CountableSupClosed t → CountableSupClosed (s ∩ t)
-- Mathlib.Topology.VectorBundle.Basic
/-- The zero section of a vector bundle is continuous at each point.  -/
Bundle.Trivialization.continuousAt_zeroSection : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [VectorBundle R F E] (x : B),
  ContinuousAt (Bundle.zeroSection F E) x
-- Init.Data.SInt.Lemmas
Int8.toISize_ne_neg_one : ∀ (a : Int8), a ≠ -1 → a.toISize ≠ -1
-- Init.Data.UInt.Bitwise
UInt32.not_xor : ∀ {a b : UInt32}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_bot : ∀ {C : ℝ} {f g : ℝ → ℝ} {l : Filter ℝ},
  Filter.Tendsto (fun x => g x / f x) l Filter.atBot → 0 < C → Asymptotics.IsBigOWith C l f g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp k (t.maxKey ⋯)).isLE = true
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.MonoidalCategory.inducingFunctorData_μIso : ∀ (R : Type u) [inst : CommRing R] (x x_1 : CoalgCat R),
  (CoalgCat.MonoidalCategory.inducingFunctorData R).μIso x x_1 =
    CategoryTheory.Iso.refl
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj x)
        ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj x_1))
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_sdiff_left : ∀ {α : Type u_1} {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ \ t ⊆ s₂ \ t
-- Init.Data.Array.Subarray
Std.Slice.Internal.SubarrayData.mk.inj : ∀ {α : Type u} {array : Array α} {start stop : ℕ} {start_le_stop : start ≤ stop}
  {stop_le_array_size : stop ≤ array.size} {array_1 : Array α} {start_1 stop_1 : ℕ} {start_le_stop_1 : start_1 ≤ stop_1}
  {stop_le_array_size_1 : stop_1 ≤ array_1.size},
  { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size } =
      { array := array_1, start := start_1, stop := stop_1, start_le_stop := start_le_stop_1,
        stop_le_array_size := stop_le_array_size_1 } →
    array = array_1 ∧ start = start_1 ∧ stop = stop_1