mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.toArray.toList = t.toList
-- Mathlib.Data.ZMod.QuotientGroup
AddAction.orbitZMultiplesEquiv_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β)
  (k : ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)),
  (AddAction.orbitZMultiplesEquiv a b).symm k = k.cast • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
-- Init.Data.Int.Basic
Int.instLEInt : LE ℤ
-- Mathlib.Order.Bounds.Defs
IsCoinitialFor.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s t : Set α), IsCoinitialFor s t = ∀ ⦃a : α⦄, a ∈ s → ∃ b ∈ t, b ≤ a
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Icc_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Icc a b)), Subtype.val '' Set.Ici c = Set.Icc (↑c) b
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Coerce an arithmetic function with values in `ℤ` to one with values in `R`. We cannot inline
this in `intCoe` because it gets unfolded too much.  -/
ArithmeticFunction.ofInt : {R : Type u_1} → [inst : AddGroupWithOne R] → ArithmeticFunction ℤ → ArithmeticFunction R
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDeriv_const_smul` without differentiability assumption when
the scalar multiplication is by division ring elements.  -/
iteratedDeriv_const_smul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F),
  iteratedDeriv n (c • f) x = c • iteratedDeriv n f x
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX)
      (CategoryTheory.SmallObject.πFunctorObj f πX) =
    πX
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePushoutShape.mkCocone.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.Limits.WidePushoutShape J → Sort u_2) →
    (j : CategoryTheory.Limits.WidePushoutShape J) → (Unit → motive none) → ((j : J) → motive (some j)) → motive j
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.lor.eq_1 : Nat.lor = Nat.bitwise or
-- Mathlib.FieldTheory.SeparableDegree
/-- If `K / E / F` is a field extension tower, such that `K / E` is algebraic,
then there is a non-canonical bijection
`Field.Emb F E × Field.Emb E K ≃ Field.Emb F K`. A corollary of `algHomEquivSigma`.  -/
Field.embProdEmbOfIsAlgebraic : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                [inst_5 : Algebra E K] →
                  [IsScalarTower F E K] → [Algebra.IsAlgebraic E K] → Field.Emb F E × Field.Emb E K ≃ Field.Emb F K
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.congr_simp : ∀ (b b_1 : ByteArray) (e_b : b = b_1) (i i_1 : ℕ) (e_i : i = i_1) (acc acc_1 : Array Char),
  acc = acc_1 → ∀ (hi : i ≤ b.size), ByteArray.utf8Decode?.go b i acc hi = ByteArray.utf8Decode?.go b_1 i_1 acc_1 ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a.fmod b < b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1) (l l_1 : List ((_ : α) × β)) (e_l : l = l_1)
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValue a l h = Std.Internal.List.getValue a_1 l_1 ⋯
-- Mathlib.Topology.MetricSpace.Bounded
totallyBounded_Ico : ∀ {α : Type u} [inst : UniformSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α), TotallyBounded (Set.Ico a b)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A), HomogeneousLocalization.mk 1 = 1
-- Mathlib.Order.Bounded
Set.Unbounded.rel_mono : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, r' ≤ r → Set.Unbounded r s → Set.Unbounded r' s
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.erase_zero : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), SkewPolynomial.erase n 0 = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_comap : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂),
  ↑(AffineSubspace.comap f s) = ⇑f ⁻¹' ↑s
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.instCoeSortType : CoeSort FinBoolAlg (Type u_1)
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance.eq_1 : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G),
  Fintype.balance f = f - Function.const ι (Finset.univ.expect fun y => f y)
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the reverse direction of `isAddTorsionFree_iff_not_isOfFinAddOrder`. -/
IsAddTorsionFree.of_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddCommGroup G], (∀ ⦃a : G⦄, a ≠ 0 → ¬IsOfFinAddOrder a) → IsAddTorsionFree G
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).inv
      (CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp f h)) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U).ι h
-- Mathlib.RingTheory.Valuation.Basic
/-- The trivial valuation, sending everything to 1 other than 0.  -/
Valuation.one : (R : Type u_3) →
  (Γ₀ : Type u_4) →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
        [Nontrivial R] → [NoZeroDivisors R] → [DecidablePred fun x => x = 0] → One (Valuation R Γ₀)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubalgebra.unitization_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S)
  (x : Unitization R ↥s), (NonUnitalSubalgebra.unitization s) x = (algebraMap R A) x.toProd.1 + ↑x.toProd.2
-- Mathlib.Topology.Compactification.StoneCech
instCompactSpaceStoneCech : ∀ {α : Type u} [inst : TopologicalSpace α], CompactSpace (StoneCech α)
-- Mathlib.RingTheory.Nilpotent.Lemmas
nilradical_eq_sInf : ∀ (R : Type u_3) [inst : CommSemiring R], nilradical R = sInf {J | J.IsPrime}
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorMap.eq_1 : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (n : ℕ),
  CategoryTheory.Limits.SequentialProduct.functorMap f n =
    CategoryTheory.Limits.Pi.map fun m =>
      if h : m < n then CategoryTheory.eqToHom ⋯
      else
        if h' : m < n + 1 then
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (f m) (CategoryTheory.eqToHom ⋯))
        else CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.forgetToTop_faithful : (CategoryTheory.forget₂ AlexDisc TopCat).Faithful
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.Model.ForwardStringSearcher.instLawfulForwardPatternModel : ∀ {pat : String}, String.Slice.Pattern.Model.LawfulForwardPatternModel pat
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_ae_eq_restrict_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β], MeasurableSet s → s.indicator f =ᵐ[μ.restrict sᶜ] 0
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instMax.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  SupBotHom.instMax =
    {
      max := fun f g =>
        have __src := f.toBotHom ⊔ g.toBotHom;
        let __SupHom := f.toSupHom ⊔ g.toSupHom;
        { toSupHom := __SupHom, map_bot' := ⋯ } }
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.re_im_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable (fun x => RCLike.re (f x)) μ ∧ MeasureTheory.Integrable (fun x => RCLike.im (f x)) μ ↔
    MeasureTheory.Integrable f μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ (-y)` tends to `0` at `+∞` for any positive real `y`.  -/
tendsto_rpow_neg_atTop : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ (-y)) Filter.atTop (nhds 0)
-- Batteries.Data.Array.Lemmas
Array.extract_empty_of_start_eq_stop : ∀ {α : Type u_1} {i : ℕ} {a : Array α}, a.extract i i = #[]
-- Mathlib.Data.Rat.Defs
Rat.isInt.eq_1 : ∀ (a : ℚ), a.isInt = (a.den == 1)
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.alls.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4)
  (φ : L.BoundedFormula α 0) (h_1 : (φ : L.BoundedFormula α 0) → motive 0 φ)
  (h_2 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → motive _n.succ φ),
  (match 0, φ with
    | 0, φ => h_1 φ
    | _n.succ, φ => h_2 _n φ) =
    h_1 φ
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanShape_L : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C],
  (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).L = CategoryTheory.OrthogonalReflection.D₂ W Z
-- Init.Data.UInt.Lemmas
UInt64.ofInt_one : UInt64.ofInt 1 = 1
-- Lean.Parser.Command
Lean.Parser.Command.noncomputable.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.subgroupClosure_mul_pow : ∀ {G : Type u_2} [inst : Group G] {s : Set G},
  s.Nonempty → ∀ (n : ℕ), ↑(Subgroup.closure s) * s ^ n = ↑(Subgroup.closure s)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Eq.sameCycle : ∀ {α : Type u_2} {x y : α}, x = y → ∀ (f : Equiv.Perm α), f.SameCycle x y
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_rid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {N' : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid N']
  [inst_6 : Module R N'] (f : N →ₗ[R] N'),
  ↑(TensorProduct.assoc R M R N') ∘ₗ TensorProduct.map (↑(TensorProduct.rid R M).symm) f =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R N).symm)
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- The kernel of the adjoint action on a Lie algebra is equal to its center.  -/
LieDerivation.ad_ker_eq_center : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (LieDerivation.ad R L).ker = LieAlgebra.center R L
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfc_nnreal : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [inst_4 : IsTopologicalRing A] [T2Space A] [inst_6 : PartialOrder A] [inst_7 : NonnegSpectrumClass ℝ A]
  [inst_8 : StarOrderedRing A] [inst_9 : ContinuousStar A] [inst_10 : StarModule ℝ A]
  [inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  0 ≤ a → (Set.range fun x => cfc x a) = {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}
-- Mathlib.NumberTheory.Divisors
Nat.image_fst_divisorsAntidiagonal : ∀ {n : ℕ}, Finset.image Prod.fst n.divisorsAntidiagonal = n.divisors
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofNat.injEq : ∀ (n n_1 : ℕ), (Lean.LeanOptionValue.ofNat n = Lean.LeanOptionValue.ofNat n_1) = (n = n_1)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i j : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i),
  MeasurableSet j → (s.toMeasureOfLEZero i hi₁ hi).real j = -s (i ∩ j)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk_of_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : N),
  Monoid.Coprod.mk (FreeMonoid.of (Sum.inr x)) = Monoid.Coprod.inr x
-- Mathlib.Order.Defs.LinearOrder
LinOrd.of.inj : ∀ {carrier : Type u_2} {str : LinearOrder carrier} {carrier_1 : Type u_2} {str_1 : LinearOrder carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'RingHom_apply : ∀ {o : Type u_4} (m' : o → Type u_7) (α : Type u_12) [inst : DecidableEq o] [inst_1 : (i : o) → DecidableEq (m' i)]
  [inst_2 : Fintype o] [inst_3 : (i : o) → Fintype (m' i)] [inst_4 : NonAssocSemiring α]
  (M : (i : o) → Matrix (m' i) (m' i) α), (Matrix.blockDiagonal'RingHom m' α) M = Matrix.blockDiagonal' M
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mk.sizeOf_spec : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SizeOf R] [inst_2 : SizeOf M] (carrier : Set M)
  (vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier),
  sizeOf { carrier := carrier, vadd_mem' := vadd_mem' } = 1
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.brecOn_1.go : {motive_1 : Lean.Parser.Tactic.MRefinePat → Sort u} →
  {motive_2 : List Lean.Parser.Tactic.MRefinePat → Sort u} →
    (t : List Lean.Parser.Tactic.MRefinePat) →
      ((t : Lean.Parser.Tactic.MRefinePat) → t.below → motive_1 t) →
        ((t : List Lean.Parser.Tactic.MRefinePat) → Lean.Parser.Tactic.MRefinePat.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Parser.Tactic.MRefinePat.below_1 t
-- Mathlib.Data.Nat.Digits.Div
Nat.modEq_eleven_digits_sum : ∀ (n : ℕ), ↑n ≡ (List.map (fun n => ↑n) (Nat.digits 10 n)).alternatingSum [ZMOD 11]
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.sub : {R : Type u} → {M : Type v} → [Sub R] → [Sub M] → Sub (TrivSqZeroExt R M)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_himp : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α} {x : α},
  x ∈ U ⇨ V ↔ ∃ W, W ⊓ U ≤ V ∧ x ∈ W
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle between three points equals the unoriented angle if the sign is
positive.  -/
EuclideanGeometry.oangle_eq_angle_of_sign_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.Order.KrullDimension
Order.height_le_height_apply_of_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictMono f → ∀ (x : α), Order.height x ≤ Order.height (f x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] (s : Finset α), ∅ - s = ∅
-- Mathlib.Algebra.Tropical.Basic
Tropical.surjective_untrop : ∀ {R : Type u}, Function.Surjective Tropical.untrop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      (m₁.diff m₂ ⋯).getD k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback else m₁.getD k fallback
-- Mathlib.Order.Disjoint
disjoint_comm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ Disjoint b a
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.toPolyN.induct_unfolding : ∀ (motive : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly → Prop),
  (∀ (a b : Lean.Grind.Linarith.Expr), motive (a.sub b) Lean.Grind.Linarith.Poly.nil) →
    (∀ (a : Lean.Grind.Linarith.Expr), motive a.neg Lean.Grind.Linarith.Poly.nil) →
      (∀ (k : ℤ) (a : Lean.Grind.Linarith.Expr),
          motive (Lean.Grind.Linarith.Expr.intMul k a) Lean.Grind.Linarith.Poly.nil) →
        motive Lean.Grind.Linarith.Expr.zero Lean.Grind.Linarith.Poly.nil →
          (∀ (v : Lean.Grind.Linarith.Var),
              motive (Lean.Grind.Linarith.Expr.var v) (Lean.Grind.Linarith.Poly.add 1 v Lean.Grind.Linarith.Poly.nil)) →
            (∀ (a b : Lean.Grind.Linarith.Expr),
                motive a a.toPolyN → motive b b.toPolyN → motive (a.add b) (a.toPolyN.combine b.toPolyN)) →
              (∀ (k : ℕ) (a : Lean.Grind.Linarith.Expr),
                  motive a a.toPolyN → motive (Lean.Grind.Linarith.Expr.natMul k a) (a.toPolyN.mul ↑k)) →
                ∀ (a : Lean.Grind.Linarith.Expr), motive a a.toPolyN
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquiv.toMonoidWithZeroHom_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] (f : G ≃* H) (x : G),
  f.toMonoidWithZeroHom x = f x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β},
  t.modify k f ≠ ∅ → (t.modify k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Mathlib.RingTheory.HopfAlgebra.Quotient
Ideal.isHopfIdeal_iff : ∀ (R : Type u_1) {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : HopfAlgebraStruct R A] (I : Ideal A),
  Ideal.IsHopfIdeal R I ↔
    (Submodule.restrictScalars R I).IsCoideal ∧ ∀ ⦃x : A⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instDiv : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Div (SpecialLinearGroup R V)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_sub_right : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N]
  (f₁ f₂ g : α →₀ N), (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A telescoping sum along `{0, ..., n - 1}` of a function valued in a commutative
additive group reduces to the difference of the last and first terms.  -/
Finset.sum_range_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n : ℕ), ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
-- Init.Data.Array.Find
Array.finIdxOf?_eq_none_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, xs.finIdxOf? a = none ↔ a ∉ xs
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
-- Mathlib.Algebra.Lie.Graded
LieDerivation.ofGradingSum_of : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ] (φ : ι →+ R)
  (i : ι) (a : ↥(ℒ i)),
  (LieDerivation.ofGradingSum ℒ φ) ((DirectSum.of (fun x => ↥(ℒ x)) i) a) = φ i • (DirectSum.of (fun x => ↥(ℒ x)) i) a
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (CochainComplex.mappingCocone.triangle φ).mor₁ = CochainComplex.mappingCocone.fst φ
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.const_equiv : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {q r : ℚ}, CauSeq.const (padicNorm p) q ≈ CauSeq.const (padicNorm p) r ↔ q = r
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Copy of a braided structure on a functor `F` with new `ε`, `μ`, `η` and `δ` fields equal to the
old ones.

This is useful to fix definitional equalities.  -/
CategoryTheory.Functor.Braided.copy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  (hF : F.Braided) →
                    (ε' :
                        CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                          F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                      (μ' :
                          (X Y : C) →
                            CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                              F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                        (η' :
                            F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                              CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                          (δ' :
                              (X Y : C) →
                                F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) →
                            autoParam (ε' = CategoryTheory.Functor.LaxMonoidal.ε F)
                                CategoryTheory.Functor.Braided.copy._auto_1 →
                              autoParam (μ' = CategoryTheory.Functor.LaxMonoidal.μ F)
                                  CategoryTheory.Functor.Braided.copy._auto_3 →
                                autoParam (η' = CategoryTheory.Functor.OplaxMonoidal.η F)
                                    CategoryTheory.Functor.Braided.copy._auto_5 →
                                  autoParam (δ' = CategoryTheory.Functor.OplaxMonoidal.δ F)
                                      CategoryTheory.Functor.Braided.copy._auto_7 →
                                    F.Braided