mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
_private.Mathlib.Topology.Algebra.IsUniformGroup.Basic.0.IsDenseInducing.extend_Z_bilin_aux : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {G : Type u_5} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α]
  [IsTopologicalAddGroup α] [inst_3 : TopologicalSpace β] [inst_4 : AddCommGroup β] [inst_5 : TopologicalSpace δ]
  [inst_6 : AddCommGroup δ] [inst_7 : UniformSpace G] [inst_8 : AddCommGroup G] {e : β →+ α},
  IsDenseInducing ⇑e →
    ∀ {φ : β →+ δ →+ G},
      (Continuous fun p => (φ p.1) p.2) →
        ∀ {W' : Set G},
          W' ∈ nhds 0 →
            ∀ (x₀ : α) (y₁ : δ),
              ∃ U₂ ∈ Filter.comap (⇑e) (nhds x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
-- Mathlib.Analysis.Normed.Group.Quotient
Ideal.Quotient.semiNormedCommRing : {R : Type u_3} → [inst : SeminormedCommRing R] → (I : Ideal R) → SeminormedCommRing (R ⧸ I)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.equiv_trans : ∀ {ι : Type u_3} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  (e : M ≃ N) (hf : e 0 = 0) (f₂ : N ≃ O) (hf₂ : f₂ 0 = 0),
  Finsupp.mapRange.equiv (e.trans f₂) ⋯ = (Finsupp.mapRange.equiv e hf).trans (Finsupp.mapRange.equiv f₂ hf₂)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap_comm : ∀ {R : Type u_1} {n : Type u_2} [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq n] (i j : n),
  Matrix.swap R i j = Matrix.swap R j i
-- Mathlib.RingTheory.Multiplicity
emultiplicity_of_isUnit_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, ¬IsUnit a → IsUnit b → emultiplicity a b = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Mathlib.Order.BoundedOrder.Basic
bot_lt_of_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, b < a → ⊥ < a
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_mul : ∀ {a b : ENNReal}, (a * b).toReal = a.toReal * b.toReal
-- Batteries.Data.Array.Basic
/-- Fold a monadic function `f` over the subarray from the right, returning the list of partial results.
 -/
Subarray.scanrM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → β → m β) → β → Subarray α → m (Array β)
-- Lean.Server.Rpc.Basic
Lean.Server.RpcObjectStore.mk.sizeOf_spec : ∀ (aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef Lean.Server.ReferencedObject)
  (refsById : Lean.PersistentHashMap USize Lean.Lsp.RpcRef) (nextRef : USize) (wireFormat : Lean.Lsp.RpcWireFormat),
  sizeOf { aliveRefs := aliveRefs, refsById := refsById, nextRef := nextRef, wireFormat := wireFormat } =
    1 + sizeOf aliveRefs + sizeOf refsById + sizeOf nextRef + sizeOf wireFormat
-- Init.Data.Repr
/-- Converts a string to its corresponding Lean string literal syntax. Double quotes are added to each
end, and internal characters are escaped as needed.

Examples:
* `"abc".quote = "\"abc\""`
* `"\"".quote = "\"\\\"\""`
 -/
String.quote : String → String
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.isUnit : ∀ (F : Type u_1) {K : Type u_2} [inst : Field F] [inst_1 : Ring K] [IsDomain K] [inst_3 : Algebra F K]
  [FiniteDimensional F K] {x : K}, x ≠ 0 → IsUnit x
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderShiftExtensionProductIterInt_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] (n : ℕ),
  (P.extensionProductIter n).IsStableUnderShift ℤ
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_injective : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P.op = Q.op → P = Q
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.continuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous fun p => p.1 ×ˢ p.2
-- Mathlib.Topology.ContinuousMap.Weierstrass
/-- An alternative statement of Weierstrass' theorem,
for those who like their epsilons.

Every real-valued continuous function on `[a,b]` is within any `ε > 0` of some polynomial.
 -/
exists_polynomial_near_continuousMap : ∀ (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)) (ε : ℝ), 0 < ε → ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_trans : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [inst_4 : MonadControl n₁ m]
  [inst_5 : MonadControlT n₂ n₁] (x : stM n₂ m α),
  ⦃ Std.Internal.Do.wp (MonadControl.restoreM (restoreM x)) post epost ⦄ restoreM x ⦃ post; epost ⦄
-- Mathlib.Topology.Order.Basic
pi_Iio_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' x' : ι → α} [Nonempty ι], (∀ (i : ι), x' i < a' i) → Set.Iio a' ∈ nhds x'
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal : ∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [NumberField K] [I.IsMaximal],
  Finite (NumberField.RingOfIntegers K ⧸ I)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Array.MinMax
/-- Returns the largest element of a non-empty array.

Examples:
* `#[4].max (by decide) = 4`
* `#[1, 4, 2, 10, 6].max (by decide) = 10`
 -/
Array.max : {α : Type u_1} → [Max α] → (arr : Array α) → arr ≠ #[] → α
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom : ∀ (n : Type u) (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S).toSpecΓ
      (AlgebraicGeometry.Spec.map
        (CommRingCat.ofHom
          (MvPolynomial.eval₂Hom
            (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace n S ↘ S)))
            (AlgebraicGeometry.AffineSpace.coord S))))
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.of_surjective : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Algebra.FiniteType R A] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → Algebra.FiniteType R B
-- Mathlib.Order.Filter.CardinalInter
cardinalInterFilter_aleph_one_iff : ∀ {α : Type u} {l : Filter α}, CardinalInterFilter l (Cardinal.aleph 1) ↔ CountableInterFilter l
-- Init.Data.String.TakeDrop
String.nextUntil : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.shiftFunctor_map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} [inst_1 : AddCommGroup β] (s : β)
  {X Y : CategoryTheory.GradedObjectWithShift s C} (f : X ⟶ Y) (t : β) (n : ℤ),
  (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).map f t = f (t + n • s)
-- Lean.DocString.Parser
/-- Items like 1.  -/
Lean.Doc.Parser.OrderedListType.numDot : Lean.Doc.Parser.OrderedListType
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.measurable_sum : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, Measurable (f i)) → Measurable fun a => ∑ i ∈ s, f i a
-- Mathlib.Algebra.Order.ToIntervalMod
/-- Reduce `b` to the interval `Ioc a (a + p)`.  -/
toIocMod : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → [hα : Archimedean α] → {p : α} → 0 < p → α → α → α
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
with a summable bound on the derivatives, then the series is differentiable.
Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
convergence then the series is zero everywhere so the result still holds.  -/
differentiable_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F},
  Summable u →
    (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) →
      (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) → Differentiable 𝕜 fun y => ∑' (n : α), f n y
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_add_mul_I : ∀ (x y : ℂ),
  Complex.sin (x + y * Complex.I) = Complex.sin x * Complex.cosh y + Complex.cos x * Complex.sinh y * Complex.I
-- Init.Data.Vector.Lemmas
Vector.any_flatten : ∀ {α : Type u_1} {n m : ℕ} {f : α → Bool} {xss : Vector (Vector α n) m}, xss.flatten.any f = xss.any fun x => x.any f
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_map : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F] {f : E →ₗ[R] F}
  {C : PointedCone R E} {y : F}, y ∈ PointedCone.map f C ↔ ∃ x ∈ C, f x = y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.diff_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.diff m₂ = m₁ \ m₂
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.one_opow : ∀ (a : Ordinal.{u_1}), 1 ^ a = 1
-- Mathlib.Order.RelIso.Basic
/-- A surjective relation embedding is a relation isomorphism.  -/
RelIso.ofSurjective : {α : Type u_1} →
  {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → (f : r ↪r s) → Function.Surjective ⇑f → r ≃r s
-- Lean.Parser.Term
Lean.Parser.Term.macroLastArg : Lean.Parser.Parser
-- Mathlib.Algebra.Free
FreeAddSemigroup.mk_add_mk : ∀ {α : Type u} (x y : α) (L1 L2 : List α),
  { head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeForwardRule : Aesop.ForwardRule → Aesop.SafeRule → Aesop.BaseRuleSetMember
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_eq_zero : ∀ {R : Type u} [inst : Semiring R] {a : AddMonoidAlgebra R ℕ}, { toFinsupp := a } = 0 ↔ a = 0
-- Mathlib.Logic.Lemmas
dite_ite_distrib_right : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a b : p → α} {c : ¬p → α},
  dite p (fun hp => if q then a hp else b hp) c = if q then dite p a c else dite p b c
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Following `Trie`s based on a `Key.labelledStar`.  -/
Lean.Meta.RefinedDiscrTree.Trie.labelledStars : {α : Type} → Lean.Meta.RefinedDiscrTree.Trie α → Std.HashMap ℕ Lean.Meta.RefinedDiscrTree.TrieIndex
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.of_head : ∀ {hd : ℝ} (tl : Tactic.ComputeAsymptotics.UnitMonomial),
  0 < hd → Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos (hd :: tl)
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- Given `(v : K), (q : ℚ), and v = q`, we have that `of q = of v`  -/
GenContFract.coe_of_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ},
  v = ↑q →
    { h := ↑(GenContFract.of q).h, s := Stream'.Seq.map (GenContFract.Pair.map Rat.cast) (GenContFract.of q).s } =
      GenContFract.of v
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instNSMul : {M : Type uM} → {N : Type uN} → [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → SMul ℕ (M →+ N)
-- Mathlib.Order.CompactlyGenerated.Basic
sSupIndep_iff_finite : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {s : Set α},
  sSupIndep s ↔ ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNatTR_eq_sModNat : ∀ (q i : ℕ), LucasLehmer.norm_num_ext.sModNatTR q i = LucasLehmer.norm_num_ext.sModNat q i
-- Mathlib.Algebra.BigOperators.Finprod
/-- Monotonicity of `finprod`. See `finprod_le_finprod'` for a variant where
`M` is an ordered `CommMonoid`.  -/
finprod_le_finprod : ∀ {α : Type u_1} {M : Type u_7} [inst : CommMonoidWithZero M] [inst_1 : PartialOrder M] [ZeroLEOneClass M]
  [PosMulMono M] {f g : α → M},
  Function.HasFiniteMulSupport f →
    (∀ (a : α), 0 ≤ f a) → Function.HasFiniteMulSupport g → f ≤ g → ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
-- Init.Control.Lawful.Instances
OptionT.run_map : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : OptionT m α),
  (f <$> x).run = Option.map f <$> x.run
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.mk.sizeOf_spec : ∀ (x : Lean.Grind.CommRing.Var) (k : ℕ), sizeOf { x := x, k := k } = 1 + sizeOf x + sizeOf k
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.mk.sizeOf_spec : ∀ (toBoolAlg : BoolAlg) [isFintype : Fintype ↑toBoolAlg],
  sizeOf { toBoolAlg := toBoolAlg, isFintype := isFintype } = 1 + sizeOf toBoolAlg + sizeOf isFintype
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderSucc_apply : ∀ {n : ℕ} (i : Fin (n + 1)), Order.succ i = Fin.lastCases (Fin.last n) Fin.succ i
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- The regulator of a number field `K`.  -/
NumberField.Units.regulator : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℝ
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_pred_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b < Order.pred a ↔ b < a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (I.subschemeCover.f U) I.subschemeι =
    CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.closure_cycleType_eq_two_two_eq_top : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → Subgroup.closure {g | (↑g).cycleType = {2, 2}} = ⊤
-- Mathlib.Algebra.Algebra.Basic
/-- **Alias** of `Module.isTorsionFree_iff_faithfulSMul`. -/
NoZeroSMulDivisors.iff_faithfulSMul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [IsDomain R] [IsDomain A],
  Module.IsTorsionFree R A ↔ FaithfulSMul R A
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.toLinearEquiv_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G),
  (LinearIsometryEquiv.lTensor E f).toLinearEquiv = LinearEquiv.lTensor E f.toLinearEquiv
-- Init.Data.Fin.Lemmas
Fin.natAdd_castAdd : ∀ (p m : ℕ) {n : ℕ} (i : Fin n), Fin.natAdd m (Fin.castAdd p i) = Fin.cast ⋯ (Fin.castAdd p (Fin.natAdd m i))
-- Mathlib.Tactic.CrossRefAttribute
/-- The name of the declaration carrying the cross-reference.  -/
Mathlib.CrossRef.Tag.declName : Mathlib.CrossRef.Tag → Lean.Name
-- Mathlib.Data.List.OffDiag
List.Perm.offDiag : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.offDiag.Perm l₂.offDiag
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → m.alter a f = m_1.alter a f_1
-- Mathlib.Tactic.GrindAttrs
/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed.
It is called by the `closedness` tactic.  -/
Lean.Parser.Attr.closedness!? : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv_left₀`. -/
Antivary.of_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → Antivary f⁻¹ g → Monovary f g
-- Init.Data.Array.Attach
Array.reverse_unattach : ∀ {α : Type u_1} {P : α → Prop} {xs : Array (Subtype P)}, xs.unattach.reverse = xs.reverse.unattach
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedState.mk.injEq : ∀ (cmdState : Lean.Elab.Command.State)
  (firstCmdSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)
  (cmdState_1 : Lean.Elab.Command.State)
  (firstCmdSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot),
  ({ cmdState := cmdState, firstCmdSnap := firstCmdSnap } =
      { cmdState := cmdState_1, firstCmdSnap := firstCmdSnap_1 }) =
    (cmdState = cmdState_1 ∧ firstCmdSnap = firstCmdSnap_1)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.comp : ∀ (R : Type u_4) [inst : CommRing R] (A : Type u_5) [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_6)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.FormallySmooth R A]
  [Algebra.FormallySmooth A B], Algebra.FormallySmooth R B
-- Init.Data.Vector.Lemmas
Vector.toList_eq_nil_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.toList = [] ↔ n = 0
-- Mathlib.Analysis.Convex.BetweenList
/-- The points in a list are strictly in that order on a line.  -/
List.Sbtw : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [PartialOrder R] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → List P → Prop
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of injective maps are injective under some flatness conditions.
Also see `TensorProduct.map_injective_of_flat_flat` and
`TensorProduct.map_injective_of_flat_flat_of_isDomain` for different flatness conditions.  -/
TensorProduct.map_injective_of_flat_flat' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {P : Type u_4} {Q : Type u_5}
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] (f : P →ₗ[R] M)
  (g : Q →ₗ[R] N) [Module.Flat R P] [Module.Flat R N],
  Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(TensorProduct.map f g)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    (∀ a ∈ t, (List.map Sigma.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Mathlib.Data.Finset.Sum
Finset.disjSum_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.homOfPath.eq_def : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] (x : G)
  (x_1 : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x),
  IsFreeGroupoid.SpanningTree.homOfPath T x_1 =
    match x, x_1 with
    | .(Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)), Quiver.Path.nil =>
      CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
    | x, p.cons f =>
      CategoryTheory.CategoryStruct.comp (IsFreeGroupoid.SpanningTree.homOfPath T p)
        (Sum.recOn (↑f) (fun e => IsFreeGroupoid.of e) fun e => CategoryTheory.inv (IsFreeGroupoid.of e))
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Given a `k`-linear `G`-representation `A`, the set of representation morphisms
`Hom(k[Gⁿ⁺¹], A)` is `k`-linearly isomorphic to the set of functions `Gⁿ → A`.  -/
Rep.diagonalHomEquiv : (k G : Type u) →
  [inst : Group G] →
    [inst_1 : CommRing k] → (n : ℕ) → (A : Rep.{u, u, u} k G) → (Rep.diagonal k G (n + 1) ⟶ A) ≃ₗ[k] (Fin n → G) → ↑A
-- Lean.Parser.Command
Lean.Parser.Command.printEqns.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Logic.Small.Set
small_iInter : ∀ {α : Type u1} {ι : Type u4} (s : ι → Set α) (i : ι) [Small.{u, u1} ↑(s i)], Small.{u, u1} ↑(⋂ i, s i)
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_of_finite : ∀ {G : Type u_3} [inst : AddGroup G] [Finite G], AddGroup.FG G
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given `R`-module X and `S`-module Y and a map `X ⟶ (restrictScalars f).obj Y`, i.e `R`-linear map
`X ⟶ Y`, there is a map `(extend_scalars f).obj X ⟶ Y`, i.e `S`-linear map `S ⨂ X → Y` by
`s ⊗ x ↦ s • g x`.
 -/
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} → (X ⟶ (ModuleCat.restrictScalars f).obj Y) → ((ModuleCat.extendScalars f).obj X ⟶ Y)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff : CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.right =
  CategoryTheory.Limits.WalkingPair.left
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Given a mono factorisation `X ⟶ I ⟶ Y` of an arrow `f` that is an image and an isomorphism `I ≅ I'`,
the induced mono factorisation by the isomorphism is also an image.
 -/
CategoryTheory.Limits.IsImage.ofIsoI : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F : CategoryTheory.Limits.MonoFactorisation f} →
          CategoryTheory.Limits.IsImage F → {I' : C} → (e : F.I ≅ I') → CategoryTheory.Limits.IsImage (F.ofIsoI e)
-- Mathlib.LinearAlgebra.DirectSum.Basis
Module.Free.directSum : ∀ (R : Type u_1) [inst : Semiring R] {ι : Type u_2} (M : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)], Module.Free R (DirectSum ι fun i => M i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], (Std.DHashMap.Const.toArray m).isEmpty = m.isEmpty