mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Range
Vector.map_zipIdx : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ},
  Vector.map (Prod.map f id) (xs.zipIdx k) = (Vector.map f xs).zipIdx k
-- Init.Data.List.Control
List.findM?_eq_findSomeM? : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α},
  List.findM? p as =
    List.findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
-- Mathlib.GroupTheory.Congruence.Hom
/-- Surjective `AddMonoid` homomorphisms constant on an additive congruence
relation `c`'s equivalence classes induce a surjective homomorphism on `c`'s quotient.  -/
AddCon.lift_surjective_of_surjective : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (h : c ≤ AddCon.ker f), Function.Surjective ⇑f → Function.Surjective ⇑(c.lift f h)
-- Mathlib.Topology.Piecewise
Continuous.if : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {p : α → Prop}
  [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ frontier {x | p x}, f a = g a) → Continuous f → Continuous g → Continuous fun a => if p a then f a else g a
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.id_pushforward : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : TopCat),
  TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (TopCat.Presheaf C X)
-- Mathlib.Condensed.Light.EffectiveEpi
instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.PreservesEpimorphisms
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_7 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℕ)
  (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.natMul k a) =
    k • Lean.Grind.Linarith.Expr.denoteN ctx a
-- Mathlib.Topology.Order.Compact
/-- `Set.Ico a b` is only compact if it is empty.  -/
isCompact_Ico_iff : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsCompact (Set.Ico a b) ↔ b ≤ a
-- Mathlib.Data.List.Infix
List.tails_eq_inits : ∀ {α : Type u_1} (l : List α), l.tails = (List.map List.reverse l.reverse.inits).reverse
-- Init.Data.Vector.Lemmas
Vector.foldl_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β},
  Vector.foldl f b xs.reverse = Vector.foldr (fun x y => f y x) b xs
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MonadInfo.mk : Lean.Expr → Lean.Level → Lean.Level → Lean.Expr → Lean.Expr → Lean.Elab.Do.MonadInfo
-- Init.Data.UInt.BasicAux
BitVec.ofNatLT.eq_1 : ∀ {w : ℕ} (i : ℕ) (p : i < 2 ^ w), i#'p = { toFin := ⟨i, p⟩ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).isEmpty = true ↔
      ∀ (k : α) (h : m.contains k = true), f k (m.get k h) = none)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValRat p q` when `q` is expressed in terms of `Rat.mk`.  -/
padicValRat.defn : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {q : ℚ} {n d : ℤ},
  q ≠ 0 → q = Rat.divInt n d → padicValRat p q = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)
-- Mathlib.Data.Nat.Count
Nat.count_injective : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → Nat.count p m = Nat.count p n → m = n
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkFun : Lean.Name → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_top : ∀ {X Y : TopCat} (f : X ⟶ Y), (TopologicalSpace.Opens.map f).obj ⊤ = ⊤
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.ker_flip_eq_bot : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → B.ker = ⊥ → B.flip.ker = ⊥
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.insert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α) (v : β k), m₁.Equiv m₂ → (m₁.insert k v).Equiv (m₂.insert k v)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Promote `HahnEmbedding.Partial.evalCoeff`'s output to a new `HahnSeries`.  -/
HahnEmbedding.Partial.eval : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                HahnEmbedding.Partial seed →
                                  [IsOrderedAddMonoid R] →
                                    [Archimedean R] → M → Lex (HahnSeries (FiniteArchimedeanClass M) R)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its line derivative at `x₀` in the direction `v` has norm bounded by `C * ‖v‖`.
Version using `lineDeriv`.  -/
norm_lineDeriv_le_of_lipschitz : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {x₀ : E} {C : NNReal}, LipschitzWith C f → ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖
-- Mathlib.Data.Fin.Fin2
/-- `n` as a member of `Fin (n + 1)`  -/
Fin2.fs : {n : ℕ} → Fin2 n → Fin2 (n + 1)
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.card_functions_sum_skolem₁_le : ∀ {L : FirstOrder.Language}, Cardinal.mk ((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max Cardinal.aleph0 L.card
-- Mathlib.Order.CompleteLattice.Basic
iInf_of_isEmpty : ∀ {α : Type u_8} {ι : Sort u_9} [inst : InfSet α] [IsEmpty ι] (f : ι → α), iInf f = sInf ∅
-- Mathlib.Algebra.Homology.Monoidal
/-- If `K₁` and `K₂` are two homological complexes, this is the property that
for all `j`, the coproduct of `K₁ i₁ ⊗ K₂ i₂` for `i₁ + i₂ = j` exists.  -/
HomologicalComplex.HasTensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
          [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
            {I : Type u_2} →
              [inst_5 : AddMonoid I] →
                {c : ComplexShape I} → [c.TensorSigns] → HomologicalComplex C c → HomologicalComplex C c → Prop
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_finsetSum : ∀ {R : Type u} {ι : Type y} [inst : Semiring R] (s : Finset ι) (g : ι → Polynomial R) (x : R),
  Polynomial.eval x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval x (g i)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorHom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).f = CategoryTheory.Limits.prod.map f.f g.f
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkYoneda` is compatible with `uliftFunctor`.  -/
CategoryTheory.shrinkYonedaUliftFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.LocallySmall.{max w w', v, u} C] →
        CategoryTheory.shrinkYoneda.{w, v, u}.comp
            ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj
              CategoryTheory.uliftFunctor.{w', w}) ≅
          CategoryTheory.shrinkYoneda.{max w w', v, u}
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instNeBotUnconditional : ∀ (β : Type u_2), (SummationFilter.unconditional β).NeBot
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projl_inr_apply : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : L},
  (LieAlgebra.SemiDirectSum.projl ψ) ((LieAlgebra.SemiDirectSum.inr ψ) x) = 0
-- Init.Core
instHasEquivOfSetoid : {α : Sort u} → [Setoid α] → HasEquiv α
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_eq_zero : ∀ {A : Type u_1} [inst : One A] {x : A}, Additive.ofMul x = 0 ↔ x = 1
-- Std.Do.SPred.Laws
Std.Do.SPred.exists_elim : ∀ {σs : List (Type u)} {α : Sort u_1} {Φ : α → Std.Do.SPred σs} {Q : Std.Do.SPred σs},
  (∀ (a : α), Φ a ⊢ₛ Q) → (∃ a, Φ a) ⊢ₛ Q
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- Build an isomorphism in the category `BialgCat R` from a
`BialgEquiv`.  -/
BialgEquiv.toBialgIso : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : Ring X] →
        [inst_2 : Ring Y] →
          [inst_3 : Bialgebra R X] → [inst_4 : Bialgebra R Y] → (X ≃ₐc[R] Y) → (BialgCat.of R X ≅ BialgCat.of R Y)
-- Mathlib.Order.Monotone.Basic
AntitoneOn.strictAntiOn_of_injOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  AntitoneOn f s → Set.InjOn f s → StrictAntiOn f s
-- Mathlib.Order.Filter.Pointwise
Filter.mulRightMono : ∀ {α : Type u_2} [inst : Mul α], MulRightMono (Filter α)
-- Mathlib.CategoryTheory.Opposites
/-- The isomorphism between `F.leftOp.rightOp` and `F`.  -/
CategoryTheory.Functor.leftOpRightOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C Dᵒᵖ) → F.leftOp.rightOp ≅ F
-- Mathlib.Topology.UniformSpace.Cauchy
/-- If `univ` is complete, the space is a complete space  -/
completeSpace_of_isComplete_univ : ∀ {α : Type u} [uniformSpace : UniformSpace α], IsComplete Set.univ → CompleteSpace α
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- If `e : ℝ≥0`, returns a proof of `0 ≤ (e : ℝ)`.  -/
Mathlib.Tactic.Linarith.mkToRealNonnegProof? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The geometric series converges if the constant term is zero.  -/
PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] {f : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → Summable fun x => f ^ x
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff_lt_of_lt_add : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    s ⊆ t →
      ∀ (ε : ℝ),
        μ.real t < μ.real s + ε →
          autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff_lt_of_lt_add._auto_1 → μ.real (t \ s) < ε
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of a measurable function is smaller than its mean, while
avoiding a null set.  -/
MeasureTheory.exists_notMem_null_le_laverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → AEMeasurable f μ → μ N = 0 → ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.insertMany t l).getKey! k' = k
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.boundedOrder : {α : Type u_1} → [inst : LE α] → [BoundedOrder α] → BoundedOrder (Multiplicative α)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.opEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.opEquivalence.counitIso = CategoryTheory.Iso.refl ((P.op.lift P.ι.op ⋯).comp (P.lift P.op.ι.leftOp ⋯).rightOp)
-- Mathlib.Algebra.Notation.Prod
Prod.instSMul : {E : Type u_8} → {α : Type u_9} → {β : Type u_10} → [SMul E α] → [SMul E β] → SMul E (α × β)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux.eq_def : ∀ (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂ =
    match fuel with
    | 0 => (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
    | fuel.succ =>
      match m₁, m₂ with
      | m₁, [] => (List.reverse r₁ ++ m₁, List.reverse r₂)
      | [], m₂ => (List.reverse r₁, List.reverse r₂ ++ m₂)
      | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ =>
        bif Nat.blt v₁ v₂ then Nat.Internal.Linear.Poly.cancelAux fuel m₁ ((k₂, v₂) :: m₂) ((k₁, v₁) :: r₁) r₂
        else
          bif Nat.blt v₂ v₁ then Nat.Internal.Linear.Poly.cancelAux fuel ((k₁, v₁) :: m₁) m₂ r₁ ((k₂, v₂) :: r₂)
          else
            bif k₁.blt k₂ then Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ ((k₂.sub k₁, v₁) :: r₂)
            else
              bif k₂.blt k₁ then Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ ((k₁.sub k₂, v₁) :: r₁) r₂
              else Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂
-- Init.Data.Vector.Count
Vector.count_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, Vector.count a #v[b] = if (b == a) = true then 1 else 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.rotate_darts : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  (c.rotate u h).darts ~r c.darts
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.prod : ∀ {𝕜 : 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] {F' : Type u_21} [inst_6 : NormedCommRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'},
  (∀ i ∈ t, MDiff (f i)) → MDiff (∏ i ∈ t, f i)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- If `0 < n`, then `QuaternionGroup n` has `4n` elements.
 -/
QuaternionGroup.card : ∀ {n : ℕ} [inst : NeZero n], Fintype.card (QuaternionGroup n) = 4 * n
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian
are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_strongDual : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [CompleteSpace E] {S : Type u_4} {X : S → Ω → E} {Y : T → Ω → E} [inst_5 : NormedSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess (Sum.elim X Y) P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (t : T), AEMeasurable (Y t) P) →
        (∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), ProbabilityTheory.covariance (⇑L₁ ∘ X s) (⇑L₂ ∘ Y t) P = 0) →
          ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.Algebra.Ring.Equiv
/-- makes a `RingHom` from the bijective inverse of a `RingHom`  -/
RingHom.inverse : {R : Type u_4} →
  {S : Type u_5} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        (f : R →+* S) → (g : S → R) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S →+* R
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.multipliable_of_le_one : ∀ {α : Type u_1} {f : α → ENNReal}, (∀ (i : α), f i ≤ 1) → Multipliable f
-- Mathlib.Order.ModularLattice
IsModularLattice.sup_inf_sup_assoc : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, (x ⊔ z) ⊓ (y ⊔ z) = (x ⊔ z) ⊓ y ⊔ z
-- Mathlib.Algebra.Algebra.Bilinear
Algebra.lmul_isUnit_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
  IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.mk : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    (toLHom : L →ᴸ L') →
      (invLHom : L' →ᴸ L) →
        invLHom.comp toLHom = FirstOrder.Language.LHom.id L →
          toLHom.comp invLHom = FirstOrder.Language.LHom.id L' → (L ≃ᴸ L')
-- Mathlib.Topology.EMetricSpace.Defs
/-- Pseudoemetric space instance on subsets of pseudoemetric spaces  -/
instPseudoEMetricSpaceSubtype : {α : Type u_2} → {p : α → Prop} → [PseudoEMetricSpace α] → PseudoEMetricSpace (Subtype p)
-- Mathlib.Analysis.CStarAlgebra.Projection
/-- An element in a non-unital C⋆-algebra is a star projection
if and only if it is idempotent and normal.  -/
isStarProjection_iff_isIdempotentElem_and_isStarNormal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  {p : A}, IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_top : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {x : R}, x ∈ ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k k' : α} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k =
      (Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.eq_1 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] (a : α), AddLECancellable a = ∀ ⦃b c : α⦄, a + b ≤ a + c → b ≤ c
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = g ≫ k` induces a morphism
`l : coequalizer f g ⟶ W` satisfying `coequalizer.π ≫ g = l`.  -/
CategoryTheory.Limits.coequalizer.desc' : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] →
          {W : C} →
            (k : Y ⟶ W) →
              CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
                { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l = k }
-- Mathlib.LinearAlgebra.StdBasis
LinearEquiv.piCongrRight.eq_1 : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} {ψ : ι → Type u_2}
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_4 : (i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i),
  LinearEquiv.piCongrRight e =
    { toFun := fun f i => (e i) (f i), map_add' := ⋯, map_smul' := ⋯, invFun := fun f i => (e i).symm (f i),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_eq_iff : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit b → (a - b = c ↔ a = c + b)
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_sphere_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rio_eq_some : ∀ {n i : ℕ}, i < n → (*...n).toArray[i]? = some i
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_map_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : LowerSet β),
  ↑((LowerSet.map f).symm s) = ⇑f ⁻¹' ↑s
-- Mathlib.NumberTheory.WellApproximable
/-- **Gallagher's ergodic theorem** on Diophantine approximation.  -/
AddCircle.addWellApproximable_ae_empty_or_univ : ∀ {T : ℝ} [hT : Fact (0 < T)] (δ : ℕ → ℝ),
  Filter.Tendsto δ Filter.atTop (nhds 0) →
    (∀ᵐ (x : AddCircle T), x ∉ addWellApproximable (AddCircle T) δ) ∨
      ∀ᵐ (x : AddCircle T), x ∈ addWellApproximable (AddCircle T) δ
-- Mathlib.Order.MinMax
max_lt_max_left_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max b c < max a c ↔ b < a ∧ c < a
-- Mathlib.Data.Finset.PImage
Part.coe_toFinset : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], ↑o.toFinset = {x | x ∈ o}
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_C_of_ne_zero : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], n ≠ 0 → (Polynomial.C a).coeff n = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.min : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {f g : δ → α},
  Measurable f → Measurable g → Measurable fun a => min (f a) (g a)
-- Std.Time.Format.Modifier
/-- Narrow form (e.g., "T")
 -/
Std.Time.Text.narrow : Std.Time.Text
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If two locally integrable functions on a finite-dimensional real vector space have the same
integral when multiplied by any smooth compactly supported function, then they coincide almost
everywhere.  -/
ae_eq_of_integral_contDiff_smul_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [inst_6 : MeasurableSpace E]
  [BorelSpace E] {f f' : E → F} {μ : MeasureTheory.Measure E},
  MeasureTheory.LocallyIntegrable f μ →
    MeasureTheory.LocallyIntegrable f' μ →
      (∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = ∫ (x : E), g x • f' x ∂μ) →
        ∀ᵐ (x : E) ∂μ, f x = f' x
-- Lean.Util.Diff
Lean.Diff.Action.noConfusionType : Sort v✝ → Lean.Diff.Action → Lean.Diff.Action → Sort v✝
-- Init.Grind.AC
Lean.Grind.AC.Seq.startsWithVar_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Lean.DefEqAttrib
/-- Marks the theorem as a definitional equality that can be used by `dsimp`.

The theorem must be an equality that holds at `.implicit` transparency. A theorem
with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`
(and also `@[backward_defeq]`, since the latter is a superset); write `:= (rfl)`
instead to suppress this.

The attribute should be given before a `@[simp]` attribute to have effect.

When using the module system, an exported theorem can only be `@[defeq]` if all
definitions that need to be unfolded to prove the theorem are exported and exposed.

Tagging a theorem with `@[defeq]` automatically also tags it with `@[backward_defeq]`,
maintaining the invariant that `@[defeq]` theorems form a subset of `@[backward_defeq]`
theorems.
 -/
Lean.defeqAttr : Lean.TagAttribute