mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Defs
ENormedCommMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedCommMonoid : ESeminormedCommMonoid E] → (∀ (x : E), ‖x‖ₑ = 0 ↔ x = 1) → ENormedCommMonoid E
-- Lean.MetavarContext
Lean.instInhabitedMetavarDecl.default : Lean.MetavarDecl
-- Mathlib.LinearAlgebra.Ray
sameRay_neg_swap : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R (-x) y ↔ SameRay R x (-y)
-- Mathlib.Algebra.Star.Module
/-- Note that this lemma holds for an arbitrary `ℚ`-action, rather than merely one coming from a
`DivisionRing`. We keep both the `qsmul` and `rat_smul` naming conventions for discoverability.
See `star_qsmul`.  -/
star_rat_smul : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : StarAddMonoid R] [inst_2 : Module ℚ R] (q : ℚ) (x : R),
  star (q • x) = q • star x
-- Init.Data.BitVec.Lemmas
BitVec.xor_left_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), x ^^^ z = y ^^^ z ↔ x = y
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.epi_iff_surjective : ∀ {A B : GrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α},
  r.iter.toArray = r.toArray
-- Mathlib.Data.Set.Image
Set.image_symmDiff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ (s t : Set α), f '' symmDiff s t = symmDiff (f '' s) (f '' t)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.toLinearEquiv_toSpanSingletonLIE : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E],
  (ContinuousLinearMap.toSpanSingletonLIE 𝕜 E).toLinearEquiv = ContinuousLinearMap.toSpanSingletonLE 𝕜 𝕜 E
-- Mathlib.Algebra.Divisibility.Basic
decompositionMonoid_iff : ∀ (α : Type u_1) [inst : Semigroup α], DecompositionMonoid α ↔ ∀ (a : α), IsPrimal a
-- Mathlib.Algebra.BigOperators.Pi
Pi.mulSingle_induction : ∀ {ι : Type u_1} [Finite ι] [inst : DecidableEq ι] {M : ι → Type u_7} [inst_1 : (i : ι) → CommMonoid (M i)]
  (p : ((i : ι) → M i) → Prop) (f : (i : ι) → M i),
  p 1 → (∀ (f g : (i : ι) → M i), p f → p g → p (f * g)) → (∀ (i : ι) (m : M i), p (Pi.mulSingle i m)) → p f
-- Mathlib.Data.Int.Init
Int.neg_nat_succ : ∀ (n : ℕ), -↑n.succ = (-↑n).pred
-- Std.Sat.AIG.CachedLemmas
/-- `mkAtomCached` does not modify the input AIG upon a cache hit.
 -/
Std.Sat.AIG.mkAtomCached_hit_aig : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {var : α} (aig : Std.Sat.AIG α)
  {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom var)},
  aig.cache.get? (Std.Sat.AIG.Decl.atom var) = some hit → (aig.mkAtomCached var).aig = aig
-- Lean.Util.PPExt
Lean.PPFns.ppConstNameWithInfos : Lean.PPFns → Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_singleR : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r).size =
    (Std.DTreeMap.Internal.Impl.bin k v (Std.DTreeMap.Internal.Impl.bin lk lv ll lr) r).size
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C},
  (h.homIso W).hom = TypeCat.ofHom fun f => (t.extend f.down).π
-- Mathlib.Control.ULift
ULift.seq_up : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), ({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemNSMul.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} [inst_1 : Fintype α] [inst_2 : DecidableEq α]
  [inst_3 : DecidablePred fun x => x ∈ s] (n : ℕ),
  Set.decidableMemNSMul n = Nat.recAux (⋯.mpr inferInstance) (fun n ih => ⋯.mpr inferInstance) n
-- Mathlib.Data.Set.Finite.Monad
Set.fintypePure : {α : Type u} → (a : α) → Fintype ↑(pure a)
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.Approx.truncate.match_1.splitter : {F : PFunctor.{u_1, u_2}} →
  (motive : (x : ℕ) → PFunctor.Approx.CofixA F (x + 1) → Sort u_3) →
    (x : ℕ) →
      (x_1 : PFunctor.Approx.CofixA F (x + 1)) →
        ((a : F.A) → (a_1 : F.B a → PFunctor.Approx.CofixA F 0) → motive 0 (PFunctor.Approx.CofixA.intro a a_1)) →
          ((a : ℕ) →
              (i : F.A) →
                (f : F.B i → PFunctor.Approx.CofixA F (a + 1)) → motive a.succ (PFunctor.Approx.CofixA.intro i f)) →
            motive x x_1
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrInvMem.mem_or_inv_mem : ∀ {S : Type u_3} {G : Type u_4} {inst : Inv G} {inst_1 : SetLike S G} (s : S) [self : HasMemOrInvMem s] (a : G),
  a ∈ s ∨ a⁻¹ ∈ s
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → UpperSet α),
  (⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.liftAt : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k m : ℕ},
  φ.IsQF → (FirstOrder.Language.BoundedFormula.liftAt k m φ).IsQF
-- Init.Data.BitVec.Bitblast
BitVec.msb_neg : ∀ {w : ℕ} {x : BitVec w}, (-x).msb = (x != 0#w && x != BitVec.intMin w ^^ x.msb)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates colimits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits of
shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesLimitsOfShape J F.op
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ), ↑(MeasureTheory.Integrable.toL1 f hf) = MeasureTheory.AEEqFun.mk f ⋯
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F), HasDerivWithinAt (⇑e) (e 1) s x
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceFrom_le_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p₀.sliceFrom q h ≤ p ↔ q ≤ String.Slice.Pos.ofSliceFrom p
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.eq_1 : ∀ {α : Type u_1} (ys : List α) (le : α → α → Bool), [].merge ys le = ys
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSum.match_1.eq_2 : ∀ {n m : ℕ} (motive : Fin n ⊕ Fin m → Sort u_1) (x : Fin m) (h_1 : (x : Fin n) → motive (Sum.inl x))
  (h_2 : (x : Fin m) → motive (Sum.inr x)),
  (match Sum.inr x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_2 x
-- Mathlib.CategoryTheory.Bicategory.Free
/-- 1-morphisms in the free bicategory.  -/
CategoryTheory.FreeBicategory.Hom : {B : Type u} → [Quiver B] → B → B → Type (max u v)
-- Mathlib.Analysis.Meromorphic.Order
/-- A finprod of functions that do not vanish locally does not vanish locally.
 -/
meromorphicOrderAt_finprod_ne_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_5} {F : ι → 𝕜 → 𝕜},
  (∀ (c : ι), MeromorphicAt (F c) x) →
    (∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤) → meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- A predicate characterizing homomorphisms between additive monoids `M` and `N` that form a
commutative triangle with the canonical map from `M` to its localization at `S` and
some isomorphism between `N` and the localization.  -/
AddSubmonoid.IsLocalizationMap : {M : Type u_1} → [inst : AddCommMonoid M] → {N : Type u_2} → [AddCommMonoid N] → AddSubmonoid M → (M → N) → Prop
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_one`. -/
upperCentralSeries_one : ∀ (G : Type u_1) [inst : Group G], Subgroup.upperCentralSeries G 1 = Subgroup.center G
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Units.Defs
/-- Copy an `AddUnit`, adjusting definitional equalities.  -/
AddUnits.copy : {α : Type u} → [inst : AddMonoid α] → (u : AddUnits α) → (val : α) → val = ↑u → (neg : α) → neg = ↑(-u) → AddUnits α
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U =
    CategoryTheory.Limits.Pi.lift fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) p.2)
        (F.map ((U p.1).infLERight (U p.2)).op)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.nnnorm_ofSubsingleton : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (f : E →L[𝕜] F),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 E F i) f‖₊ = ‖f‖₊
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Multiplying `0` by a scalar gives `0`  -/
DistribMulAction.smul_zero : ∀ {M : Type u_12} {A : Type u_13} {inst : Monoid M} {inst_1 : AddMonoid A} [self : DistribMulAction M A] (a : M),
  a • 0 = 0
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.withoutShareCommonChecks : {m : Type → Type u_1} → {α : Type} → [MonadWithReaderOf Lean.Meta.Sym.Context m] → m α → m α
-- Mathlib.Order.Interval.Finset.Box
/-- Hollow box centered at `0 : α` going from `-n` to `n`.  -/
Finset.box : {α : Type u_1} → [Ring α] → [inst : PartialOrder α] → [LocallyFiniteOrder α] → [DecidableEq α] → ℕ → Finset α
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The `i`-th row of a Young diagram consists of the cells whose first coordinate is `i`.  -/
YoungDiagram.row : YoungDiagram → ℕ → Finset (ℕ × ℕ)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instInterOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Inter (Std.ExtHashSet α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic.0.Real.sqrtTwoAddSeries.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.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.Approx.truncate.match_1.eq_1 : ∀ {F : PFunctor.{u_1, u_2}} (motive : (x : ℕ) → PFunctor.Approx.CofixA F (x + 1) → Sort u_3) (a : F.A)
  (a_1 : F.B a → PFunctor.Approx.CofixA F 0)
  (h_1 : (a : F.A) → (a_2 : F.B a → PFunctor.Approx.CofixA F 0) → motive 0 (PFunctor.Approx.CofixA.intro a a_2))
  (h_2 :
    (a : ℕ) →
      (i : F.A) → (f : F.B i → PFunctor.Approx.CofixA F (a + 1)) → motive a.succ (PFunctor.Approx.CofixA.intro i f)),
  (match 0, PFunctor.Approx.CofixA.intro a a_1 with
    | 0, PFunctor.Approx.CofixA.intro a a_2 => h_1 a a_2
    | a.succ, PFunctor.Approx.CofixA.intro i f => h_2 a i f) =
    h_1 a a_1
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableEmbedding_inv : ∀ {α : Type u_3} {m : MeasurableSpace α} [inst : InvolutiveInv α] [MeasurableInv α], MeasurableEmbedding Inv.inv
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.i : {n : Type u_1} → {R : Type u₂} → Matrix.TransvectionStruct n R → n
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.splitter : (motive : Turing.PartrecToTM2.Cont' → Sort u_1) →
  (x : Turing.PartrecToTM2.Cont') →
    ((fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k)) →
      ((k : Turing.PartrecToTM2.Cont') → motive k.cons₂) →
        ((f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k)) →
          ((f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k)) →
            (Unit → motive Turing.PartrecToTM2.Cont'.halt) → motive x
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFun_map_fun_finsetSum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : InnerProductSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) P) =
        ∏ i ∈ s, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.edgeSet_bot : ∀ {α : Type u_1} {β : Type u_2}, ⊥.edgeSet = ∅
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.equalizer_toSubsemiring : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (ϕ ψ : A →ₐ[R] B),
  (ϕ.equalizer ψ).toSubsemiring =
    { carrier := {a | ϕ a = ψ a}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.precomp_mk₀_injective_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (L : C) {M N : C} (g : M ⟶ N) [hg : CategoryTheory.Epi g],
  Function.Injective ⇑((CategoryTheory.Abelian.Ext.mk₀ g).precomp L ⋯)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.congrLeft_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (R : Type u_10) {W : Type u_11} [inst_7 : Ring R]
  [inst_8 : AddCommGroup W] [inst_9 : Module k W] [inst_10 : Module R W] [inst_11 : SMulCommClass k R W]
  (e : P₁ ≃ᵃ[k] P₂) (Q : Type u_12) [inst_12 : AddTorsor W Q] (f : P₂ →ᵃ[k] Q) (x : P₁),
  ((AffineEquiv.congrLeft R e Q).symm f) x = f (e x)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.mk.inj : ∀ {heq : Bool} {hIdx xIdx : ℕ} {heq_1 : Bool} {hIdx_1 xIdx_1 : ℕ},
  { heq := heq, hIdx := hIdx, xIdx := xIdx } = { heq := heq_1, hIdx := hIdx_1, xIdx := xIdx_1 } →
    heq = heq_1 ∧ hIdx = hIdx_1 ∧ xIdx = xIdx_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {Y : C} {g : Y ⟶ S} (hf : CategoryTheory.Presieve.ofArrows X f g),
  g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f hf.idx)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, k ∈ m.insertIfNew k v
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instMonoOfMkLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.Mono (CategoryTheory.Subobject.ofMkLEMk f g h)
-- Mathlib.Data.Sym.Sym2
/-- `s(x, y)` is an unordered pair,
which is to say a pair modulo the action of the symmetric group.

It is equal to `Sym2.mk (x, y)`.  -/
«termS(_,_)» : Lean.ParserDescr
-- Mathlib.RingTheory.Filtration
/-- **Alias** of `Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree`. -/
Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  [IsDomain R] [IsNoetherianRing R] [Module.IsTorsionFree R M] [Module.Finite R M], I ≠ ⊤ → ⨅ i, I ^ i • ⊤ = ⊥
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.mul : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : ArithmeticFunction R},
  f.IsMultiplicative → g.IsMultiplicative → (f * g).IsMultiplicative
-- Init.Core
Sum.inr.injEq : ∀ {α : Type u} {β : Type v} (val val_1 : β), (Sum.inr val = Sum.inr val_1) = (val = val_1)
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.monotoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s → ∀ {a : α}, a ∈ s → MonotoneOn (variationOnFromTo f s a) s
-- Init.Data.String.Lemmas.Basic
String.sliceFrom_sliceFrom : ∀ {s : String} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos},
  (s.sliceFrom pos).sliceFrom pos' = s.sliceFrom (String.Pos.ofSliceFrom pos')
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_map : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N),
  (LinearMap.rTensor Q f') ((TensorProduct.map f g) x) = (TensorProduct.map (f' ∘ₗ f) g) x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.eq_zero_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R},
  p = 0 ↔ ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d p = 0
-- Init.Core
ForInStep.yield.injEq : ∀ {α : Type u} (a a_1 : α), (ForInStep.yield a = ForInStep.yield a_1) = (a = a_1)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- Any two `IsAddKleinFour` groups are isomorphic via any
equivalence which sends the identity of one group to the identity of the other.  -/
IsAddKleinFour.addEquiv : {G₁ : Type u_2} →
  {G₂ : Type u_3} →
    [inst : AddGroup G₁] →
      [inst_1 : AddGroup G₂] → [IsAddKleinFour G₁] → [IsAddKleinFour G₂] → (e : G₁ ≃ G₂) → e 0 = 0 → G₁ ≃+ G₂
-- Init.Data.List.ToArray
List.back?_toArray : ∀ {α : Type u_1} (l : List α), l.toArray.back? = l.getLast?
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.factor_dvd_of_not_isUnit : ∀ {K : Type v} [inst : Field K] {f : Polynomial K}, ¬IsUnit f → f.factor ∣ f
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.comp_toOrderHom : ∀ {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c),
  SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.comp f g) =
    (SimplexCategory.Hom.toOrderHom g).comp (SimplexCategory.Hom.toOrderHom f)
-- Mathlib.Topology.DerivedSet
IsClosed.relDerivedSet_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Set X}, IsClosed A → relDerivedSet A = derivedSet A
-- Mathlib.Geometry.Manifold.Algebra.Monoid
smoothLeftMul.congr_simp : ∀ {𝕜 : 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] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] (g g_1 : G),
  g = g_1 → ∀ [inst_7 : ContMDiffMul I (↑⊤) G], smoothLeftMul I g = smoothLeftMul I g_1
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone fun x => Set.Ioi (f x)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {I : Ideal A},
  Ideal.IsHomogeneous 𝒜 I → (Ideal.homogeneousHull 𝒜 I).toIdeal = I
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.val_run_step_toIterM_iter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {z : Std.DTreeMap.Internal.RxcIterator α β},
  ↑{ internalState := z }.toIterM.step.run.inflate = z.step