mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f f_1 : M →ₛₗ[σ₁₂] M₂),
  f = f_1 → ∀ (p p_1 : Submodule R M), p = p_1 → Submodule.map f p = Submodule.map f_1 p_1
-- Lean.ToExpr
Lean.instToExprListOfToLevel : {α : Type u} → [Lean.ToLevel] → [Lean.ToExpr α] → Lean.ToExpr (List α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y_1).left.right.as =
    PUnit.unit
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [Subsingleton α], Order.krullDim α = 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_index_single_self_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ), (MvPowerSeries.coeff fun₀ | s => 1) (MvPowerSeries.X s) = 1
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_exact_iff : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔
    ∀ (x₂ : ↑S.X₂),
      (CategoryTheory.ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (CategoryTheory.ConcreteCategory.hom S.f) x₁ = x₂
-- Mathlib.CategoryTheory.Filtered.Basic
/-- a cofiltered category must be non-empty  -/
CategoryTheory.IsCofiltered.nonempty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofiltered C], Nonempty C
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Split the token at newline boundaries to support LSP clients such as VS Code that can't deal with
newline-spanning tokens.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.splitStr : Lean.FileMap → Lean.Syntax → Array Lean.Syntax
-- Mathlib.Data.Seq.Computation
Computation.think.eq_1 : ∀ {α : Type u} (c : Computation α), c.think = ⟨Stream'.cons none ↑c, ⋯⟩
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.op_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y), h.op.i = h.r.op
-- Mathlib.Order.Heyting.Hom
HeytingHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : HeytingAlgebra α] →
      [inst_1 : HeytingAlgebra β] →
        (toLatticeHom : LatticeHom α β) →
          toLatticeHom.toFun ⊥ = ⊥ →
            (∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) → HeytingHom α β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.eq_zero_of_vecMul_eq_zero : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R}
  [NoZeroDivisors R], M.det ≠ 0 → ∀ {v : m → R}, Matrix.vecMul v M = 0 → v = 0
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.mk.injEq : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  (val : F.obj (Opposite.op j))
  (map_zero : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀)
  (map_succ :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val))
  (map_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val,
            ⋯⟩)
  (val_1 : F.obj (Opposite.op j))
  (map_zero_1 : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 = val₀)
  (map_succ_1 :
    ∀ (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1 =
        d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1))
  (map_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val_1 =
        d.lift i hi
          ⟨fun x =>
            match x with
            | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val_1,
            ⋯⟩),
  ({ val := val, map_zero := map_zero, map_succ := map_succ, map_limit := map_limit } =
      { val := val_1, map_zero := map_zero_1, map_succ := map_succ_1, map_limit := map_limit_1 }) =
    (val = val_1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.insertManyIfNewUnit l).Equiv (t₂.insertManyIfNewUnit l)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.left = iY.inv
-- Std.Net.Addr
Std.Net.SocketAddressV6.mk : Std.Net.IPv6Addr → UInt16 → Std.Net.SocketAddressV6
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.isIntegral_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  {x : ↥S}, IsIntegral K x ↔ IsIntegral K ↑x
-- Init.Data.Nat.Gcd
Nat.gcd_sub_mul_right_right : ∀ {m n k : ℕ}, k * m ≤ n → m.gcd (n - k * m) = m.gcd n
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterM m α → Sort u_3) →
      (it : Std.IterM m α) →
        (Unit → motive { internalState := { list := [] } }) →
          ((x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }) → motive it
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_antitone : ∀ {X : AlgebraicGeometry.Scheme}, Antitone AlgebraicGeometry.Scheme.IdealSheafData.support
-- Init.Data.SInt.Lemmas
Int64.toInt_sub : ∀ (a b : Int64), (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 64)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.is_coprod_iff_isPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X E Y YE : C} (c : CategoryTheory.Limits.BinaryCofan X E)
  (hc : CategoryTheory.Limits.IsColimit c) {f : X ⟶ Y} {iY : Y ⟶ YE} {fE : c.pt ⟶ YE},
  CategoryTheory.CommSq f c.inl iY fE →
    (Nonempty
        (CategoryTheory.Limits.IsColimit
          (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp c.inr fE) iY)) ↔
      CategoryTheory.IsPushout f c.inl iY fE)
-- Mathlib.CategoryTheory.Center.Localization
/-- The morphism of rings `CatCenter C →+* CatCenter D` when `L : C ⥤ D`
is an additive localization functor between preadditive categories.  -/
CategoryTheory.CatCenter.localizationRingHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              [inst_3 : CategoryTheory.Preadditive C] →
                [inst_4 : CategoryTheory.Preadditive D] →
                  [L.Additive] → CategoryTheory.CatCenter C →+* CategoryTheory.CatCenter D
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_inter_ground_eq : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), M.contract (C ∩ M.E) = M.contract C
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_mul_left_iff : ∀ {R : Type u_1} {x y : R} [inst : Semiring R],
  Commute x y → x ∈ nonZeroDivisorsLeft R → (IsNilpotent (x * y) ↔ IsNilpotent y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertIfNew_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} {v : β k}, (↑(m₁.insertIfNew k v)).Equiv ↑(m₂.insertIfNew k v)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.gcd_mul_addOrderOf_div_eq : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ}
  (m : ℕ), 0 < n → m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- If a point in a topological group has a compact neighborhood, then the group is
locally compact.  -/
IsCompact.locallyCompactSpace_of_mem_nhds_of_group : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {K : Set G},
  IsCompact K → ∀ {x : G}, K ∈ nhds x → LocallyCompactSpace G
-- Mathlib.Algebra.CharP.Defs
ringChar.of_eq : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ}, ringChar R = p → CharP R p
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.poly_eq_of_wittPolynomial_bind_eq : ∀ (p : ℕ) [Fact (Nat.Prime p)] (f g : ℕ → MvPolynomial ℕ ℤ),
  (∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)) → f = g
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.orderIsoIsTwoSided_symm_apply : ∀ {R : Type u_1} [inst : Ring R] (I : { I // I.IsTwoSided }),
  (RelIso.symm TwoSidedIdeal.orderIsoIsTwoSided) I =
    have this := ⋯;
    (↑I).toTwoSided
-- Mathlib.Topology.Algebra.Field
/-- If `f` is a function `α → 𝕜` which is continuous on a preconnected set `S`, and
`f ^ 2 = 1` on `S`, then either `f = 1` on `S`, or `f = -1` on `S`.  -/
IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq : ∀ {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {S : Set α} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace 𝕜]
  [T1Space 𝕜] [inst_3 : Ring 𝕜] [NoZeroDivisors 𝕜],
  IsPreconnected S → ContinuousOn f S → Set.EqOn (f ^ 2) 1 S → Set.EqOn f 1 S ∨ Set.EqOn f (-1) S
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β k},
      (m.insert k v).toList.Perm (⟨k, v⟩ :: List.filter (fun x => decide ¬(k == x.fst) = true) m.toList)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_uIoc_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.uIoc (Fin.natAdd m i) (Fin.natAdd m j) = Set.uIoc i j
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.equiv.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit), hc.equiv = hc.equiv
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffWithinAt.clm_postcomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃}
  {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.postcomp F₁ (f y)) s x
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.isStationary : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α] [WellFoundedLT α] [Nonempty α],
  Order.cof α ≠ Cardinal.aleph0 → IsClub s → IsStationary s
-- Mathlib.ModelTheory.Substructures
/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under function symbols, then `p` holds for all elements of the closure of `s`.  -/
FirstOrder.Language.Substructure.closure_induction : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {p : M → Prop} {x : M},
  x ∈ (FirstOrder.Language.Substructure.closure L).toFun s →
    (∀ x ∈ s, p x) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (Set.ofPred p)) → p x
-- Mathlib.Order.OrderDual
/-- Transfer `Compl` across an `Equiv`.  -/
Equiv.compl : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Compl β] → Compl α
-- Init.Data.String.Basic
String.utf8ByteSize_sliceFrom : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).utf8ByteSize = s.utf8ByteSize - p.offset.byteIdx
-- Mathlib.Data.Set.Image
Set.preimage_const : ∀ {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [inst : Decidable (b ∈ s)],
  (fun x => b) ⁻¹' s = if b ∈ s then Set.univ else ∅
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_le_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u
-- Mathlib.Topology.Sober
genericPoint_specializes : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α] (x : α),
  genericPoint α ⤳ x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk_surjective : ∀ {X : SSet} (x : X.N), ∃ n y, x = SSet.N.mk ↑y ⋯
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option ((_ : α) × β) → Sort u_3) →
      (x : Option ((_ : α) × β)) → (Unit → motive none) → ((p : (_ : α) × β) → motive (some p)) → motive x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.ae_mem_iff_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ((∀ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s = μ Set.univ)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf_neBot_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ((l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s i ∩ s').Nonempty)
-- Mathlib.Order.Filter.Basic
Filter.mem_sup : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapSetEmbedding_indep_iff' : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : ↑M.E ↪ β} {I : Set β},
  (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instFunLike : (k : Type u_1) →
  {V1 : Type u_2} →
    (P1 : Type u_3) →
      {V2 : Type u_4} →
        (P2 : Type u_5) →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → FunLike (P1 →ᵃ[k] P2) P1 P2
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- Pull back a uniform space structure by an embedding, adjusting the new uniform structure to
make sure that its topology is defeq to the original one.  -/
Topology.IsEmbedding.comapUniformSpace : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [u : UniformSpace β] → (f : α → β) → Topology.IsEmbedding f → UniformSpace α
-- Mathlib.Data.Nat.ModEq
Nat.add_mod_add_ite : ∀ (a b c : ℕ), ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
-- Mathlib.Topology.Algebra.Monoid
continuousAt_nsmul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] (x : M) (n : ℕ),
  ContinuousAt (fun x => n • x) x
-- Mathlib.Data.List.Basic
List.idxOf_cons_ne : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a b : α} (l : List α),
  b ≠ a → List.idxOf a (b :: l) = (List.idxOf a l).succ
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_a₂ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).a₂ = ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)
-- Mathlib.Data.Finset.Sum
Finset.toRight_union : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u ∪ v).toRight = u.toRight ∪ v.toRight
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.id.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  [inst_1 : Wₗ.ContainsIdentities] [inst_2 : Wᵣ.ContainsIdentities] (c : C),
  CategoryTheory.Span.id c = CategoryTheory.Span.id c
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f)
      (CategoryTheory.Limits.imageSubobject f).arrow =
    f
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `R` be a nonarchimedean ring, let `f : α → R` be a function that sums to `a : R`,
and let `g : β → R` be a function that sums to `b : R`. Then `fun i : α × β ↦ f i.1 * g i.2`
sums to `a * b`.  -/
HasSum.mul_of_nonarchimedean : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] {f : α → R} {g : β → R} {a b : R},
  HasSum f a → HasSum g b → HasSum (fun i => f i.1 * g i.2) (a * b)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The long root `β`.  -/
RootPairing.EmbeddedG2.longRoot : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → [P.EmbeddedG2] → M
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.exists_lsub_cof : ∀ (o : Ordinal.{u}), ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = o.cof
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_of_tendsto_one : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
  Filter.Tendsto (u / v) l (nhds 1) → Asymptotics.IsEquivalent l u v
-- Mathlib.Data.Int.Init
Int.ediv_of_neg_of_pos : ∀ {a b : ℤ}, a < 0 → 0 < b → a.ediv b = -((-a - 1) / b + 1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_inf : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Clopens α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_natCast_cpow_of_pos : ∀ {n : ℕ}, 0 < n → ∀ (s : ℂ), ‖↑n ^ s‖ = ↑n ^ s.re
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.center_top : ∀ {α : Type u_1}, ⊤.center = Set.univ
-- Batteries.Data.Char.Basic
/-- Returns `true` if `p` returns true for some `Char`.  -/
Char.any : (Char → Bool) → Bool
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.map_i_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g) (F : CategoryTheory.Functor C D),
  (h.map F).i.left = F.map (CategoryTheory.Arrow.Hom.left h.i)
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.of_compHom : ∀ (R : Type u) (A : Type w) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : MulAction A M], IsScalarTower R A M
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinLM_eq_integral : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.IntegrableOn φ (↑K) μ →
    ∀ {f : ContDiffMapSupportedIn E F₁ n K},
      (ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ) f = ∫ (x : E), (B (f x)) (φ x) ∂μ
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.repr_injective : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι], Function.Injective OrthonormalBasis.repr
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.transpose_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : Mul α] (A B : Matrix m n α),
  (A.hadamard B).transpose = A.transpose.hadamard B.transpose
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.closure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (s : Set S),
  Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_subset_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {f g : X ⟶ Y}, f = g ↔ f.val = g.val
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The set of all statements in a Turing machine, plus one extra value `none` representing the
halt state. This is used in the TM1 to TM0 reduction.  -/
Turing.TM1.stmts : {Γ : Type u_1} →
  {Λ : Type u_2} → {σ : Type u_3} → (Λ → Turing.TM1.Stmt Γ Λ σ) → Finset Λ → Finset (Option (Turing.TM1.Stmt Γ Λ σ))
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.dualEquiv_unitIso : FinPartOrd.dualEquiv.unitIso =
  CategoryTheory.NatIso.ofComponents (fun X => FinPartOrd.Iso.mk (OrderIso.dualDual ↑X.toPartOrd))
    @FinPartOrd.dualEquiv._proof_1
-- Mathlib.Algebra.Algebra.Basic
algebraMap_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] (r : R) (m : M),
  (algebraMap R A) r • m = r • m
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedRing R] [HasSummableGeomSeries R]
  [inst_5 : NormedAlgebra 𝕜 R] {h : E → R} {S : Set E},
  DifferentiableOn 𝕜 h S → (∀ x ∈ S, IsUnit (h x)) → DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S