mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomainAddMonoidHom.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f),
  AddMonoidAlgebra.comapDomainAddMonoidHom f hf =
    { toFun := AddMonoidAlgebra.comapDomain f hf, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
IsUniformGroup.comap : ∀ {G : Type u_1} {H : Type u_2} {hom : Type u_3} [inst : Group G] [inst_1 : Group H] {u : UniformSpace H}
  [IsUniformGroup H] [inst_3 : FunLike hom G H] [MonoidHomClass hom G H] (f : hom), IsUniformGroup G
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_uInt16ToNat : ∀ (n : UInt16), UInt32.ofNatClamp n.toNat = n.toUInt32
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_iInter : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {ι : Type u_7} (s : ι → Set α), Finsupp.supported M R (⋂ i, s i) = ⨅ i, Finsupp.supported M R (s i)
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.leftOrthogonal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) (X : C), P.leftOrthogonal X ↔ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P Y → f = 0
-- Mathlib.Order.Filter.Map
Filter.neBot_of_comap : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β}, (Filter.comap m g).NeBot → g.NeBot
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one : ∀ {p t : ℝ}, 0 < t → Set.EqOn (p.rpowIntegrand₀₁ t) (fun x => t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Set.Ici 0)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_zero_left : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), ⁅0, g⁆ = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
/-- If `a ^ n ≤ b < (a + 1) ^ n`, then `n` root of `b` equals `a`.  -/
Nat.nthRoot_eq_of_le_of_lt : ∀ {n a b : ℕ}, a ^ n ≤ b → b < (a + 1) ^ n → n.nthRoot b = a
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.pi_inner : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A]
  (x y : WithCStarModule A ((i : ι) → E i)), inner A x y = ∑ i, inner A (x i) (y i)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.nil : ∀ {n : ℕ}, Nat.Primrec'.Vec fun x => List.Vector.nil
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ab_exact_iff : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.Exact ↔
    ∀ (x₂ : ↑S.X₂),
      (CategoryTheory.ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (CategoryTheory.ConcreteCategory.hom S.f) x₁ = x₂
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- An additive Lie group is a group and a `C^n` manifold at the same time in which
the addition and negation operations are `C^n`.  -/
LieAddGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (G : Type u_4) → [AddGroup G] → [inst : TopologicalSpace G] → [ChartedSpace H G] → Prop
-- Batteries.Data.List.Lemmas
List.Sublist.erase_diff_erase_sublist : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α},
  l₁.Sublist l₂ → ((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff l₁)
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_map_sectR : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (c : α) (a b : β),
  Finset.map (Function.Embedding.sectR c β) (Finset.uIcc a b) = Finset.uIcc (c, a) (c, b)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_pos_of_pos_of_dvd : ∀ {a b : ℤ}, 0 < a → 0 ≤ b → b ∣ a → 0 < a / b
-- Init.Data.UInt.Basic
/-- Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.div : UInt16 → UInt16 → UInt16
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_of_dvd_right : ∀ {m k : ℕ} (n : ℕ), m ∣ k → n.lcm m ∣ n.lcm k
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.containsₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.containsₘ a = Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- `IntermediateField.extendScalars.orderIso` bundles `IntermediateField.extendScalars`
into an order isomorphism from
`{ E : IntermediateField K L // F ≤ E }` to `IntermediateField F L`. Its inverse is
`IntermediateField.restrictScalars`.  -/
IntermediateField.extendScalars.orderIso : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (F : IntermediateField K L) → { E // F ≤ E } ≃o IntermediateField (↥F) L
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  (h : k ∈ m), m.getKey k h = k
-- Lean.CoreM
Lean.Core.instMonadInfoTreeCoreM : Lean.Elab.MonadInfoTree Lean.CoreM
-- Lean.Server.References
/-- Represents a direct import of a module in the references data structure.  -/
Lean.Server.ModuleImport : Type
-- Mathlib.Topology.Sets.VietorisTopology
/-- The Vietoris topology on the nonempty compact subsets of a topological space.  -/
TopologicalSpace.NonemptyCompacts.topology : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.coeff_add_of_supDegree_le`. -/
AddMonoidAlgebra.apply_add_of_supDegree_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p q : AddMonoidAlgebra R A} [inst_3 : AddZeroClass A] [inst_4 : Add B],
  (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
    ∀ [AddLeftStrictMono B] [AddRightStrictMono B],
      Function.Injective D →
        ∀ {ap aq : A},
          AddMonoidAlgebra.supDegree D p ≤ D ap →
            AddMonoidAlgebra.supDegree D q ≤ D aq → (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
-- Mathlib.Algebra.Quaternion
Quaternion.star_eq_two_re_sub : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a = ↑(2 * a.re) - a
-- Mathlib.Topology.MetricSpace.Basic
MulOpposite.instMetricSpace : {α : Type u_2} → [MetricSpace α] → MetricSpace αᵐᵒᵖ
-- Mathlib.GroupTheory.Congruence.Defs
/-- Multiplicative congruence relations preserve inversion.  -/
Con.inv : ∀ {M : Type u_1} [inst : Group M] (c : Con M) {x y : M}, c x y → c x⁻¹ y⁻¹
-- Mathlib.Tactic.ReduceModChar
/-- The tactic `reduce_mod_char` looks for numeric expressions in characteristic `p`
and reduces these to lie between `0` and `p`.

For example:
```
example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
```

It also handles negation, turning it into multiplication by `p - 1`,
and similarly subtraction.

This tactic uses the type of the subexpression to figure out if it is indeed of positive
characteristic, for improved performance compared to trying to synthesise a `CharP` instance.
The variant `reduce_mod_char!` also tries to use `CharP R n` hypotheses in the context.
(Limitations of the typeclass system mean the tactic can't search for a `CharP R n` instance if
`n` is not yet known; use `have : CharP R n := inferInstance; reduce_mod_char!` as a workaround.)
 -/
Tactic.ReduceModChar.reduce_mod_char : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.nonsingular_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → W.Nonsingular (W.add P Q)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.of_iso : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit c → ∀ (e : c ≅ c'), CategoryTheory.IsVanKampenColimit c'
-- Mathlib.Data.Fin.Basic
Fin.strong_induction_on : ∀ {n : ℕ} {motive : Fin n → Prop}, (∀ (j : Fin n), (∀ k < j, motive k) → motive j) → ∀ (i : Fin n), motive i
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `OrderedAdd` instance with `IsPreorder` if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.orderedAddInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_abs_abs`. -/
Asymptotics.IsBigOWith.of_abs_abs : ∀ {α : Type u_1} {c : ℝ} {l : Filter α} {u v : α → ℝ},
  (Asymptotics.IsBigOWith c l (fun x => |u x|) fun x => |v x|) → Asymptotics.IsBigOWith c l u v
-- Init.Prelude
/-- If two heterogeneously equal terms have the same type, then they are propositionally equal.  -/
eq_of_heq : ∀ {α : Sort u} {a a' : α}, a ≍ a' → a = a'
-- Init.Data.List.Scan.Lemmas
List.scanl_append : ∀ {β : Type u_1} {α : Type u_2} {b : β} {f : β → α → β} {l₁ l₂ : List α},
  List.scanl f b (l₁ ++ l₂) = List.scanl f b l₁ ++ (List.scanl f (List.foldl f b l₁) l₂).tail
-- Mathlib.RingTheory.Flat.Rank
RingHom.finrank_comp_right_of_bijective : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T),
  Function.Bijective ⇑f →
    g.Finite →
      g.Flat →
        ∀ (y : PrimeSpectrum R) (x : PrimeSpectrum S), y = PrimeSpectrum.comap f x → (g.comp f).finrank y = g.finrank x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Augmented cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Augmented : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Logic.Equiv.Sum
Equiv.emptySum_symm_apply : ∀ (α : Type u_9) (β : Type u_10) [inst : IsEmpty α] (a : β), (Equiv.emptySum α β).symm a = Sum.inr a
-- Init.Data.List.Lemmas
List.all_reverse : ∀ {α : Type u_1} {f : α → Bool} {l : List α}, l.reverse.all f = l.all f
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology `S.homology` of a short complex is
the cokernel of the morphism `S.toCycles : S.X₁ ⟶ S.cycles`.  -/
CategoryTheory.ShortComplex.homologyIsCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasHomology] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.homologyπ ⋯)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.pap.sizeOf_spec : ∀ (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg), sizeOf (Lean.IR.Expr.pap c ys) = 1 + sizeOf c + sizeOf ys
-- Mathlib.Data.Set.Lattice.Image
Set.range_eq_iUnion : ∀ {α : Type u_1} {ι : Sort u_9} (f : ι → α), Set.range f = ⋃ i, {f i}
-- Init.Core
ge_iff_le : ∀ {α : Type u_1} [inst : LE α] {x y : α}, x ≥ y ↔ y ≤ x
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.tensorProduct : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [inst_3 : CommRing R'] [inst_4 : Algebra R R'] [NoZeroDivisors R']
  [FaithfulSMul R R'], Algebra.IsAlgebraic R' (TensorProduct R R' S)
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.bijective_of_surjective_of_injective : ∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M] {N : Type w} [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (i f : N →ₗ[R] M),
  Function.Injective ⇑i → Function.Surjective ⇑f → Function.Bijective ⇑f
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveYonedaObj_obj_carrier : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (Y : C) (X : Cᵒᵖ),
  ↑((CategoryTheory.preadditiveYonedaObj Y).obj X) = (Opposite.unop X ⟶ Y)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Spec is a faithful functor.  -/
AlgebraicGeometry.Spec.faithful : AlgebraicGeometry.Scheme.Spec.Faithful
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- **Alias** of the reverse direction of `threeAPFree_image`.

---

Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
ThreeAPFree.image : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s A : Set α} {t : Set β}
  {f : α → β}, IsAddFreimanIso 2 s t f → A ⊆ s → ThreeAPFree A → ThreeAPFree (f '' A)
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [T.IsEquivalence] [B.IsEquivalence] [CategoryTheory.IsIso w.natTrans], w.GuitartExact
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_le_op_iff : ∀ {M : Type u_2} [inst : Mul M] {S₁ S₂ : Subsemigroup M}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdxD.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : ℕ) (x_1 : α), Std.DTreeMap.Internal.Impl.leaf.keyAtIdxD x x_1 = x_1
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.pow` -/
MeromorphicOn.fun_pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → ∀ (n : ℕ), MeromorphicOn (fun i => s i ^ n) U
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_iff_mul_left_eq : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
      h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- Mathlib.Data.List.Basic
List.filter_false : ∀ {α : Type u} (l : List α), List.filter (fun x => false) l = []
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.all_string_eq_all_toSlice : ∀ {pat : String} {s : String.Slice}, s.all pat = s.all pat.toSlice
-- Mathlib.Topology.Algebra.UniformMulAction
/-- An additive action such that for all `c`, the map `fun x ↦ c +ᵥ x` is uniformly continuous.  -/
UniformContinuousConstVAdd : (M : Type v) → (X : Type x) → [UniformSpace X] → [VAdd M X] → Prop
-- Mathlib.SetTheory.Cardinal.Aleph
/-- For the theorem `lift ω = ω`, see `lift_omega0`.  -/
Ordinal.lift_omega : ∀ (o : Ordinal.{u}), Ordinal.lift.{v, u} (Ordinal.omega o) = Ordinal.omega (Ordinal.lift.{v, u} o)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_add_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y : ℕ × K),
  PerfectClosure.mk K p x + PerfectClosure.mk K p y =
    PerfectClosure.mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 + (⇑(frobenius K p))^[x.1] y.2)
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.noConfusionType : Sort v✝ → Batteries.Tactic.Lint.LintVerbosity → Batteries.Tactic.Lint.LintVerbosity → Sort v✝
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_mono : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {s t : Set A}, s ⊆ t → NonUnitalStarAlgebra.adjoin R s ≤ NonUnitalStarAlgebra.adjoin R t
-- Lean.Expr
/-- Return `true` if `e` is of the form `outParam _`  -/
Lean.Expr.isOutParam : Lean.Expr → Bool
-- Init.Data.List.Lemmas
List.concat_inj_right : ∀ {α : Type u_1} {l : List α} {a a' : α}, l.concat a = l.concat a' ↔ a = a'
-- Init.Data.List.Lemmas
List.prod_reverse : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.Commutative fun x1 x2 => x1 * x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] (xs : List α),
  xs.reverse.prod = xs.prod
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContinuousMapClassContMDiffMonoidMorphism : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : Monoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], ContinuousMapClass (ContMDiffMonoidMorphism I I' n G G') G G'
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.getStruct : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.Linear.Struct
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_compat_left : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (a * c) (b * c)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.gc_map_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N] {f : M →L[R] N},
  GaloisConnection (ClosedSubmodule.map f) (ClosedSubmodule.comap f)
-- Mathlib.LinearAlgebra.Contraction
/-- The natural left-handed pairing between a module and its dual.  -/
contractLeft : (R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R (Module.Dual R M) M →ₗ[R] R
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.ringHom_of_comp_eq : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [inst_3 : CommRing S] [inst_4 : CommRing B]
  [inst_5 : Algebra S B] [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  AlgebraicIndependent R x →
    Function.Surjective ⇑f →
      Function.Injective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → AlgebraicIndependent S (⇑g ∘ x)
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.isRegularEpi_of_extremalEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.ExtremalEpi f], CategoryTheory.IsRegularEpi f
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA],
  (∀ {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y),
      J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f) →
    J.WEqualsLocallyBijective A
-- Lean.Parser.Basic
Lean.Parser.setLhsPrecFn : ℕ → Lean.Parser.ParserFn
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {β : ι → Type u_6} [m : (x : ι) → MeasurableSpace (β x)]
  (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepFun f μ =
    ProbabilityTheory.Kernel.iIndepFun f (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_map_right_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.right = φ.τ₄
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_eq_match_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.least? with
    | none => #[]
    | some least => (least...r.upper).toArray
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_ne_zero_iff : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_7} [inst : Zero α] [inst_1 : CommMonoidWithZero β] [Nontrivial β]
  [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β}, f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
-- Mathlib.Data.Matrix.Basic
/-- `piEquiv` as an `AddEquiv`.  -/
Matrix.piAddEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {ι : Type u_14} →
      {β : ι → Type u_15} → [inst : (i : ι) → Add (β i)] → Matrix m n ((i : ι) → β i) ≃+ ((i : ι) → Matrix m n (β i))
-- Init.Core
Option.some.injEq : ∀ {α : Type u} (val val_1 : α), (some val = some val_1) = (val = val_1)
-- Mathlib.Logic.Equiv.Prod
Equiv.coe_prodUnique : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β], ⇑(Equiv.prodUnique α β) = Prod.fst