mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.isInteger_or_isInteger : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {K : Type u_2} [inst_2 : Field K] [inst_3 : Algebra R K]
  [IsFractionRing R K] [h : ValuationRing R] (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
-- Mathlib.Data.Rat.Lemmas
Rat.ofNat_add_den : ∀ (n : ℕ) (q : ℚ), (OfNat.ofNat n + q).den = q.den
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_eq_bot : ∀ {α : Type u_2} [Nontrivial α] [inst : LinearOrder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] (a : WithBot α),
  a.succ = ⊥ ↔ a = ⊥
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smul_monomial : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (a : S) (n : ℕ) (b : R),
  a • (Polynomial.monomial n) b = (Polynomial.monomial n) (a • b)
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.assertHypothesisS.tacticBuilder : Lean.MVarId →
  Lean.Meta.Hypothesis → Lean.Meta.TransparencyMode → Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryFinFinset_apply : ∀ {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [inst : CommSemiring R] [inst_1 : AddCommMonoid M']
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M'] [inst_4 : Module R M₂] {k l n : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') M₂) (mk : Fin k → M') (ml : Fin l → M'),
  (((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) mk) ml =
    f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred 1
-- Mathlib.Tactic.Linter.HaveILetI
/-- The `haveILetI` linter flags uses of the `haveI` or `letI` tactic in a proof of a
proposition. Since proofs are irrelevant, the value-inlining behaviour of `haveI`/`letI`
can have no effect there, and `have`/`let` should be used instead.  -/
Mathlib.Linter.HaveILetI.linter.style.haveILetI : Lean.Option Bool
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ico_of_Icc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Icc (a i) (b i)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomHomRightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.AddMonObj X],
  CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.Algebra.Module.Torsion.Free
IsRegular.smul_eq_zero_iff_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M], IsRegular r → (r • m = 0 ↔ m = 0)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ≅ Y), f.op.unop = f
-- Lean.Meta.Tactic.Simp.Arith.Util
_private.Lean.Meta.Tactic.Simp.Arith.Util.0.Lean.Meta.Simp.Arith.isSupportedType : Lean.Expr → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.event : Lean.Lsp.SymbolKind
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (pt : C) (π : (CategoryTheory.Functor.const J).obj pt ⟶ F) (pt_1 : C)
  (π_1 : (CategoryTheory.Functor.const J).obj pt_1 ⟶ F),
  ({ pt := pt, π := π } = { pt := pt_1, π := π_1 }) = (pt = pt_1 ∧ π ≍ π_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] (l : List ((a : α) × β a)), m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_zpow_right`. -/
Equiv.Perm.SameCycle.zpow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x y → f.SameCycle x ((f ^ n) y)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_smul_monoidHom_apply : ∀ {M : Type u_5} {A : Type u_7} {B : Type u_8} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A]
  [inst_3 : MulOneClass B] (c : M) (f : A →* B) (a : A), (DomMulAct.mk c • f) a = f (c • a)
-- Mathlib.Analysis.Convex.EGauge
le_egauge_smul_right : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (c : 𝕜)
  (s : Set E) (x : E), ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)
-- Mathlib.ModelTheory.ElementarySubstructures
/-- Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.  -/
FirstOrder.Language.Substructure.toElementarySubstructure : {L : FirstOrder.Language} →
  {M : Type u_1} →
    [inst : L.Structure M] →
      (S : L.Substructure M) →
        (∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M),
            φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)) →
          L.ElementarySubstructure M
-- Mathlib.CategoryTheory.Square
/-- The functor `(Square C)ᵒᵖ ⥤ Square Cᵒᵖ`.  -/
CategoryTheory.Square.opFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Square C)ᵒᵖ (CategoryTheory.Square Cᵒᵖ)
-- Std.Data.HashSet.Raw
/-- Transforms the hash set into a list of elements in some order.  -/
Std.HashSet.Raw.toList : {α : Type u} → Std.HashSet.Raw α → List α
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instDistribMulAction : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          {𝕜 : Type u_5} →
            [inst_2 : Monoid 𝕜] →
              [inst_3 : AddMonoid γ] →
                [inst_4 : ContinuousAdd γ] →
                  [inst_5 : DistribMulAction 𝕜 γ] → [ContinuousConstSMul 𝕜 γ] → DistribMulAction 𝕜 (α →ₘ[μ] γ)
-- Mathlib.Algebra.Group.Hom.Basic
MulHom.comp_mul : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Mul M] [inst_1 : CommSemigroup N] [inst_2 : CommSemigroup P]
  (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N), g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
-- Mathlib.Analysis.Calculus.DSlope
dslope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : 𝕜} (f : 𝕜 → E), b ≠ a → dslope f a b = slope f a b
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_sub_left_iff : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E} (c : ℝ),
  autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_sub_left_iff._auto_1 →
    (IntervalIntegrable (fun x => f (c - x)) MeasureTheory.volume (c - a) (c - b) ↔
      IntervalIntegrable f MeasureTheory.volume a b)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = t.keys.head?
-- Mathlib.Combinatorics.Enumerative.Composition
/-- To `c : Composition n`, one can associate a `CompositionAsSet n` by registering the leftmost
point of each block, and adding a virtual point at the right of the last block.  -/
Composition.toCompositionAsSet : {n : ℕ} → Composition n → CompositionAsSet n
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.monoidWithZeroHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β],
  MonoidWithZeroHomClass (α →*₀ β) α β
-- Mathlib.Tactic.Polynomial.Basic
/-- Infer base ring for `Polynomial R`  -/
Mathlib.Tactic.Polynomial.polynomialInferBase : Mathlib.Tactic.Polynomial.PolynomialExt
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr : ∀ (m n : ℕ) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n),
  lhs' = lhs → rhs' = rhs → lhs.sshiftRight' rhs = lhs'.sshiftRight' rhs'
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Auxiliary definition for `pullFunctor`.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {p : S' ⟶ S} →
                  {ι' : Type t'} →
                    {X' : ι' → C} →
                      {f' : (j : ι') → X' j ⟶ S'} →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (∀ (j : ι'),
                                CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                  CategoryTheory.CategoryStruct.comp (f' j) p) →
                              F.DescentData f → F.DescentData f'
-- Mathlib.Tactic.FunProp.FunctionData
/-- Turn `MaybeFunctionData` to the function.  -/
Mathlib.Meta.FunProp.MaybeFunctionData.get : Mathlib.Meta.FunProp.MaybeFunctionData → Lean.MetaM Lean.Expr
-- Init.Notation
/-- `a ≥ b` is an abbreviation for `b ≤ a`.  -/
«term_>=_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) {X₂ Y₂ : C₂}
  (f : X₂ ⟶ Y₂) (X₃ : C₃),
  (((CategoryTheory.Functor.curry₃.obj F).obj X₁).map f).app X₃ =
    F.map (CategoryTheory.CategoryStruct.id X₁, f, CategoryTheory.CategoryStruct.id X₃)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The underlying morphism  -/
CategoryTheory.AddMod.Hom.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.AddMonObj A] → {M N : CategoryTheory.AddMod D A} → M.Hom N → (M.X ⟶ N.X)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.exists_isNClique_cliqueNum : ∀ {α : Type u_3} {G : SimpleGraph α}, ∃ s, G.IsNClique G.cliqueNum s
-- Mathlib.Analysis.Convex.Strict
strictConvex_uIcc : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.uIcc r s)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk : {Γ : Type u_1} →
  {R : Type u_2} →
    [inst : PartialOrder Γ] → [inst_1 : Zero R] → (coeff : Γ → R) → (Function.support coeff).IsPWO → HahnSeries Γ R
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_iUnion_congr_of_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_8} [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ⊆ t i) → (∀ (i : ι), μ (t i) ≤ μ (s i)) → μ (⋃ i, s i) = μ (⋃ i, t i)
-- Mathlib.Control.ULiftable
WriterT.instULiftableULiftULift : {s : Type u₀} →
  {m : Type (max u₀ v₀) → Type u_5} →
    {m' : Type (max u₀ v₁) → Type u_6} →
      [ULiftable m m'] → ULiftable (WriterT (ULift.{max v₀ u₀, u₀} s) m) (WriterT (ULift.{max v₁ u₀, u₀} s) m')
-- Init.Data.UInt.Lemmas
USize.zero_le : ∀ {a : USize}, 0 ≤ a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.copy : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_mono : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
  {n m : ℕ} {ω : Ω}, n ≤ m → MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N m ω
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.exists_mem_sup : ∀ {N : Type u_4} [inst : AddCommMonoid N] {P : N → Prop} {s t : AddSubmonoid N},
  (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ + x₂)
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.add_eq_two_iff : ∀ {n m : WithBot ℕ}, n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
-- Mathlib.FieldTheory.Normal.Closure
/-- A normal closure is always normal.  -/
IsNormalClosure.normal : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [h : IsNormalClosure F K L], Normal F L
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_mem_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α} {b : β},
  b ∈ s → a +ᵥ b ∈ a +ᵥ s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_ratCast : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → DivisionRing (G i)] [inst_7 : DivisionRing C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [∀ (i : ι), RingHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (q : ℚ),
  DirectLimit.lift f (fun x => ⇑(g x)) h ↑q = ↑q
-- Init.Prelude
/-- "Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`,
is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as
`if c then t else e` except that `t` is allowed to depend on a proof `h : c`,
and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis,
even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches.
For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
to avoid the bounds check inside the if branch. (Of course in this case we have only
lifted the check into an explicit `if`, but we could also use this proof multiple times
or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
 -/
dite : {α : Sort u} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → α
-- Mathlib.Data.TypeVec
TypeVec.append1_cases_append1 : ∀ {n : ℕ} {C : TypeVec.{u_1} (n + 1) → Sort u} (H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β))
  (α : TypeVec.{u_1} n) (β : Type u_1), TypeVec.append1Cases H (α ::: β) = H α β
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.of_finite : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, s.Finite → IsSemilinearSet s
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.compl_image_coe : ∀ {X : Type u_1} (s : Set X), (OnePoint.some '' s)ᶜ = OnePoint.some '' sᶜ ∪ {OnePoint.infty}
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_zero' : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] (g : α → F)
  (l : Filter α), Asymptotics.IsBigOWith 0 l (fun _x => 0) g
-- Mathlib.Data.Quot
Quotient.surjective_liftOn' : ∀ {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} {f : α → φ} (h : ∀ (a b : α), s₁ a b → f a = f b),
  (Function.Surjective fun x => x.liftOn' f h) ↔ Function.Surjective f
-- Mathlib.RingTheory.Flat.Basic
/-- If `M₂` and `N₁` are flat `R`-modules, `i₁ : M₁ →ₗ[R] N₁` and `i₂ : M₂ →ₗ[R] N₂` are injective
linear maps, then the linear map `i : M ≅ M₁ ⊗[R] M₂ →ₗ[R] N₁ ⊗[R] N₂ ≅ N` induced by `i₁`
and `i₂` is injective.
See `IsTensorProduct.map_injective_of_flat'` for different flatness conditions.  -/
IsTensorProduct.map_injective_of_flat_right_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7}
  {N₂ : Type u_8} [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₁] [inst_8 : Module R M₂]
  [inst_9 : AddCommMonoid N₁] [inst_10 : AddCommMonoid N₂] [inst_11 : Module R N₁] [inst_12 : Module R N₂]
  {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g)
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂),
  Function.Injective ⇑i₁ →
    Function.Injective ⇑i₂ → ∀ [Module.Flat R M₂] [Module.Flat R N₁], Function.Injective ⇑(hf.map hg i₁ i₂)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousMap.integral_apply : ∀ {X : Type u_1} {Y : Type u_2} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedAddCommGroup E] [inst_2 : TopologicalSpace Y] [inst_3 : CompactSpace Y] [inst_4 : NormedSpace ℝ E]
  [CompleteSpace E] {f : X → C(Y, E)},
  MeasureTheory.Integrable f μ → ∀ (y : Y), (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ
-- Lean.Declaration
Lean.instInhabitedConstantVal.default : Lean.ConstantVal
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumLift_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom G) (g : F.Hom G)
  (a : E.I₀ ⊕ F.I₀), (CategoryTheory.PreZeroHypercover.sumLift f g).s₀ a = Sum.elim f.s₀ g.s₀ a
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The cocone of topological modules associated to a cocone over the underlying modules, where
the cocone point is given the coinduced topology. This is colimiting when the given cocone is.  -/
TopModuleCat.ofCocone : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_1, u_2} J] →
          {F : CategoryTheory.Functor J (TopModuleCat R)} →
            CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))) →
              CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcHom_le : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] {a : A}
  (ha : p a), (cfcHom ha).range ≤ StarAlgebra.elemental 𝕜 a
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex : ∀ (n m : ℕ),
  CategoryTheory.IsIso
    (CategoryTheory.Limits.prodComparison SSet.hoFunctor (SSet.stdSimplex.obj { len := n })
      (SSet.stdSimplex.obj { len := m }))
-- Std.Data.HashSet.Lemmas
Std.HashSet.not_mem_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, a ∉ Std.HashSet.emptyWithCapacity c
-- Mathlib.Order.Minimal
OrderEmbedding.maximal_mem_image : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} (f : α ↪o β),
  Maximal (fun x => x ∈ s) x → Maximal (fun x => x ∈ ⇑f '' s) (f x)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.instFunLike : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → FunLike (A.Copy B) α β
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.overEquivalence_inverse_obj_right_as : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (W : TopologicalSpace.Opens ↥U),
  (U.overEquivalence.inverse.obj W).right.as = PUnit.unit
-- Init.Data.SInt.Bitwise
Int64.xor_right_inj : ∀ {a b : Int64} (c : Int64), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens)
  (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE g U V e₁)
      (AlgebraicGeometry.Scheme.Hom.appLE f V W e₂) =
    AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app_assoc : ∀ {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 F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) {Z : C} (h : G.obj (F'.obj x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj1.unit.app x)
      (CategoryTheory.CategoryStruct.comp (G.map ((adj1.leftAdjointUniq adj2).hom.app x)) h) =
    CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_utf8EncodeChar_eq_twoMore : ∀ {c : Char},
  c.utf8Size = 3 →
    ByteArray.utf8DecodeChar?.parseFirstByte (String.utf8EncodeChar c)[0] = ByteArray.utf8DecodeChar?.FirstByte.twoMore
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_floor_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  Nat.floor ⁻¹' {0} = Set.Iio 1