mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Map
/-- The pushforward of a submodule by an injective linear map is
linearly equivalent to the original submodule. See also `LinearEquiv.submoduleMap` for a
computable version when `f` has an explicit inverse.  -/
Submodule.equivMapOfInjective : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] →
                            (f : M →ₛₗ[σ₁₂] M₂) →
                              Function.Injective ⇑f → (p : Submodule R M) → ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map f p)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids `S, T` respectively, if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
we have `f.map hy k z + k (g y) = k (g x)` where `x : M, y ∈ S` are such that
`z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.map_add_right : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N),
  (f.map hy k) z + k (g ↑(f.sec z).2) = k (g (f.sec z).1)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (P Q : IsDedekindDomain.HeightOneSpectrum R),
  P ≠ Q → ∀ (n m : ℕ), IsCoprime (P.asIdeal ^ n) (Q.asIdeal ^ m)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.BVPred.bitblast.eq_1 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (w : ℕ)
  (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinPred) (rhs : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVPred.bitblast aig { val := Std.Tactic.BVDecide.BVPred.bin lhs op rhs, cache := cache } =
    match Std.Tactic.BVDecide.BVExpr.bitblast aig { val := lhs, cache := cache } with
    | { result := ⟨{ aig := aig_1, vec := lhsRefs }, hlhs⟩, cache := cache } =>
      match Std.Tactic.BVDecide.BVExpr.bitblast aig_1 { val := rhs, cache := cache } with
      | { result := ⟨{ aig := aig_2, vec := rhsRefs }, hrhs⟩, cache := cache } =>
        let lhsRefs_1 := lhsRefs.cast hrhs;
        match op with
        | Std.Tactic.BVDecide.BVBinPred.eq =>
          let res := Std.Tactic.BVDecide.BVPred.mkEq aig_2 { lhs := lhsRefs_1, rhs := rhsRefs };
          have cache := cache.cast ⋯;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache }
        | Std.Tactic.BVDecide.BVBinPred.ult =>
          let res := Std.Tactic.BVDecide.BVPred.mkUlt aig_2 { lhs := lhsRefs_1, rhs := rhsRefs };
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (n m : ℕ)
  (h : autoParam (m ≤ n) CategoryTheory.SimplicialObject.Truncated.trunc._auto_1)
  (G : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) (X : (SimplexCategory.Truncated m)ᵒᵖ),
  ((CategoryTheory.SimplicialObject.Truncated.trunc C n m h).obj G).obj X =
    G.obj (Opposite.op ((SimplexCategory.Truncated.incl m n ⋯).obj (Opposite.unop X)))
-- Mathlib.Algebra.Star.StarProjection
/-- `q - p` is a star projection iff `q * p = p`.  -/
IsStarProjection.sub_iff_mul_eq_right : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : StarRing R] [IsAddTorsionFree R] {p q : R},
  IsStarProjection p → IsStarProjection q → (IsStarProjection (q - p) ↔ q * p = p)
-- Mathlib.Order.Filter.Basic
/-- Either `f = ⊥` or `Filter.NeBot f`. This is a version of `eq_or_ne` that uses `Filter.NeBot`
as the second alternative, to be used as an instance.  -/
Filter.eq_or_neBot : ∀ {α : Type u} (f : Filter α), f = ⊥ ∨ f.NeBot
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddActionOreLocalization : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → AddAction (AddOreLocalization S R) (AddOreLocalization S X)
-- Init.Data.String.Lemmas.Modify
_private.Init.Data.String.Lemmas.Modify.0.String.map.eq_1 : ∀ (f : Char → Char) (s : String), String.map f s = String.mapAux f s s.startPos
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.eq_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : X ⟶ Y),
  f = h.to_ Y
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.tidy.sizeOf_spec : ∀ {s : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} (j : Lean.Elab.Tactic.Omega.Justification s c),
  sizeOf j.tidy = 1 + sizeOf s + sizeOf c + sizeOf j
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Measurable equivalence between `ULift α` and `α`.  -/
MeasurableEquiv.ulift : {α : Type u} → [inst : MeasurableSpace α] → ULift.{v, u} α ≃ᵐ α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams : Type
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β), f.comp (BoundedOrderHom.id α) = f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' → (Std.HashMap.filterMap f m).getD k fallback = (m[k]?.bind (f k')).getD fallback
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_preOmega : ∀ (o : Ordinal.{u}), Ordinal.lift.{v, u} (Ordinal.preOmega o) = Ordinal.preOmega (Ordinal.lift.{v, u} o)
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- A non-unital star subsemiring is a non-unital subsemiring which also is closed under the
`star` operation.  -/
NonUnitalStarSubsemiring : (R : Type v) → [NonUnitalNonAssocSemiring R] → [Star R] → Type v