mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSucc.congr_simp : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] {i : ℕ} {a a_1 : S} (e_a : a = a_1) (a_mem : a ∈ P ^ i),
  p.quotientToQuotientRangePowQuotSucc P a_mem = p.quotientToQuotientRangePowQuotSucc P ⋯
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.Algebra.eq_of_fg_of_subtype_eq : ∀ {R : Type u_1} {S : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {A : Subalgebra R S},
  A.FG →
    ∀ {t t' : TensorProduct R (↥A) N},
      (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t' →
        ∃ B,
          ∃ (hAB : A ≤ B),
            B.FG ∧
              (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
                (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
-- Mathlib.Data.Complex.Basic
Complex.re_add_im : ∀ (z : ℂ), ↑z.re + ↑z.im * Complex.I = z
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.isBase_of_minimal : ∀ {α : Type u_2} {M : Matroid α} {X : Set α}, M.Spanning X → (∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y) → M.IsBase X
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.iInf_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [IsEmpty ι] [inst_2 : InfSet α] (f : ι → WithTop α), ⨅ i, f i = ⊤
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.continue.sizeOf_spec : ∀ (e? : optParam (Option Lean.Meta.Simp.Result) none), sizeOf (Lean.Meta.Simp.Step.continue e?) = 1 + sizeOf e?
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {U : CategoryTheory.Comonad C}
  {c c' : CategoryTheory.Cokleisli U} {x y : c.Hom c'}, x.of = y.of → x = y
-- Mathlib.Topology.Homotopy.Path
/-- Given `F : Homotopy p q`, and `f : C(X, Y)`, we can define a homotopy from `p.map f.continuous` to
`q.map f.continuous`.
 -/
Path.Homotopy.map : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {x₀ x₁ : X} → {p q : Path x₀ x₁} → p.Homotopy q → (f : C(X, Y)) → (p.map ⋯).Homotopy (q.map ⋯)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_iff_smul_rearrangement`.

---

Two functions antivary iff the rearrangement inequality holds.  -/
AntivaryOn.smul_add_smul_le_smul_add_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Mathlib.Data.Set.Image
Set.exists_subtype_range_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↑(Set.range f) → Prop}, (∃ a, p a) ↔ ∃ i, p ⟨f i, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isQuotientCoveringMap_zpow : ∀ (n : ℤ) [NeZero n], IsQuotientCoveringMap (fun x => x ^ n) ↥(zpowGroupHom n).ker
-- Mathlib.Data.Seq.Defs
/-- Convert a sequence which is known not to terminate into a stream  -/
Stream'.Seq.toStream : {α : Type u} → (s : Stream'.Seq α) → ¬s.Terminates → Stream' α
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instSMulCoeOfSMulMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            {G : Type u_4} →
              [inst_1 : (i : ι) → SMul G (R i)] →
                [∀ (i : ι), SMulMemClass (S i) G (R i)] → SMul G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.CategoryTheory.DifferentialObject
/-- A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero
morphisms can be lifted to a functor `DifferentialObject S C ⥤ DifferentialObject S D`.  -/
CategoryTheory.Functor.mapDifferentialObject : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            (D : Type u') →
              [inst_4 : CategoryTheory.Category.{v', u'} D] →
                [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] →
                  [inst_6 : CategoryTheory.HasShift D S] →
                    (F : CategoryTheory.Functor C D) →
                      ((CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) →
                        (∀ (c c' : C), F.map 0 = 0) →
                          CategoryTheory.Functor (CategoryTheory.DifferentialObject S C)
                            (CategoryTheory.DifferentialObject S D)
-- Init.Data.String.Lemmas.Order
String.Pos.next_ne : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p.next h ≠ p
-- Mathlib.Algebra.Group.End
AddAut.neg_apply_self : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), (-e) (e m) = m
-- Mathlib.Algebra.CubicDiscriminant
Cubic.instInhabited : {R : Type u_1} → [Inhabited R] → Inhabited (Cubic R)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.MulSubshift.mk.injEq : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : Monoid G] (carrier : Set (G → A))
  (isClosed : IsClosed carrier) (mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier carrier)
  (carrier_1 : Set (G → A)) (isClosed_1 : IsClosed carrier_1)
  (mapsTo_1 : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier_1 carrier_1),
  ({ carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } =
      { carrier := carrier_1, isClosed := isClosed_1, mapsTo := mapsTo_1 }) =
    (carrier = carrier_1)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.coconeTypes_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)),
  F.coconeTypes.ι = fun j => F.ιColimitType j
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_eq_union_iff_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRatUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
      (i j : Fin (f.insertRatUnits units).1.ratUnits.size),
      i ≠ j → (f.insertRatUnits units).1.ratUnits[i] ≠ (f.insertRatUnits units).1.ratUnits[j]
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense] {Z : CategoryTheory.Functor C D}
  (h : F.comp (CategoryTheory.Functor.id D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.leftKanExtensionUnit F)
      (CategoryTheory.CategoryStruct.comp (F.whiskerLeft (CategoryTheory.Functor.IsDense.leftKanExtensionIso F).hom)
        h) =
    CategoryTheory.CategoryStruct.comp F.rightUnitor.inv h
-- Init.Data.String.Substring
/-- Converts a `Substring.Raw` into a `String.Slice`, returning `none` if the substring is invalid.
 -/
Substring.Raw.toSlice? : Substring.Raw → Option String.Slice
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.comap_top : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B]
  (f : F), NonUnitalStarSubalgebra.comap f ⊤ = ⊤
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).ediv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
-- Init.Prelude
Append.mk : {α : Type u} → (α → α → α) → Append α
-- Mathlib.Order.Filter.Defs
/-- The inverse map of a filter. A set `s` belongs to `Filter.comap m f` if either of the following
equivalent conditions hold.

1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `kernImage m s = {y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `Filter.mem_comap'`.
3. The set `(m '' sᶜ)ᶜ` belongs to `f`, see `Filter.mem_comap_iff_compl` and
   `Filter.compl_mem_comap`.
 -/
Filter.comap : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter β → Filter α
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- A cylinder object `P` is good if the morphism
`P.i : A ⨿ A ⟶ P.I` is a cofibration.  -/
HomotopicalAlgebra.Cylinder.IsGood : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.Cylinder A →
          [CategoryTheory.Limits.HasBinaryCoproduct A A] → [HomotopicalAlgebra.CategoryWithCofibrations C] → Prop
-- Mathlib.Order.Defs.LinearOrder
max_eq_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = b
-- Lean.Meta.Tactic.Grind.Extension
/-- `grind` is parametrized by a collection of `ExtensionState`. The motivation is to allow
users to use multiple extensions simultaneously without merging them into a single structure.
The collection is scanned linearly. In practice, we expect the array to be very small.
 -/
Lean.Meta.Grind.ExtensionStateArray : Type
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_zsmul : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (z : ℤ),
  ⇑(z • s) = z • ⇑s
-- Mathlib.Analysis.Calculus.Implicit
/-- **Alias** of `ImplicitFunctionData.rightFun_implicitFunction`. -/
ImplicitFunctionData.right_map_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (p : F × G) in nhds (φ.prodFun φ.pt), φ.rightFun (φ.implicitFunction p.1 p.2) = p.2
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_mul : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {m : ℕ} {a x : A},
  x ∈ I → DividedPowers.OfInvertibleFactorial.dpow I m (a * x) = a ^ m * DividedPowers.OfInvertibleFactorial.dpow I m x
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.token : Lean.Parser.Token → Lean.Parser.ParserExtension.OLeanEntry
-- Lean.Parser.Basic
Lean.Parser.instInhabitedParserCategory.default : Lean.Parser.ParserCategory
-- Mathlib.CategoryTheory.Sites.Types
/-- Given a sheaf `S` on the category of types, construct a map
`(α → S(*)) → S(α)` that is inverse to `eval`.  -/
CategoryTheory.typesGlue : (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) →
  CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S →
    (α : Type u) → (α → S.obj (Opposite.op PUnit.{u + 1})) → S.obj (Opposite.op α)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg_iff : ∀ {b x : ℝ}, 1 < b → 0 < x → (Real.logb b x < 0 ↔ x < 1)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.instInnerRegularOfIsFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [h : μ.InnerRegularCompactLTTop] [MeasureTheory.IsFiniteMeasure μ], μ.InnerRegular
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.instInhabitedSimpKind.default : Lean.Elab.Tactic.SimpKind
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_subsingleton_inter_right : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Subsingleton → t.Subsingleton
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.Convex.Star
starConvex_sInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {S : Set (Set E)}, (∀ s ∈ S, StarConvex 𝕜 x s) → StarConvex 𝕜 x (⋂₀ S)
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm_neg_add_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖-b + a‖ ≤ r
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.edge_lastDart : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil), (p.lastDart hp).edge = s(p.penultimate, w)
-- Mathlib.RepresentationTheory.Maschke
MonoidAlgebra.exists_leftInverse_of_injective : ∀ {k : Type u_1} [inst : Field k] {G : Type u_2} [Finite G] [NeZero ↑(Nat.card G)] [inst_3 : Group G] {V : Type u_3}
  [inst_4 : AddCommGroup V] [inst_5 : Module (MonoidAlgebra k G) V] {W : Type u_4} [inst_6 : AddCommGroup W]
  [inst_7 : Module (MonoidAlgebra k G) W] (f : V →ₗ[MonoidAlgebra k G] W), f.ker = ⊥ → ∃ g, g ∘ₗ f = LinearMap.id
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMatComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D] {E : Type u_2}
  [inst_4 : CategoryTheory.Category.{v₁, u_2} E] [inst_5 : CategoryTheory.Preadditive E]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] (G : CategoryTheory.Functor D E) [inst_7 : G.Additive]
  (X : CategoryTheory.Mat_ C), (F.mapMatComp G).inv.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.obj X)
-- Init.Data.Fin.Basic
Fin.modn_lt : ∀ {n m : ℕ} (i : Fin n), m > 0 → ↑(i.modn m) < m
-- Mathlib.Algebra.Group.Hom.Defs
Subsingleton.of_zeroHomClass : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [Subsingleton M] [ZeroHomClass F M N], Subsingleton F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon : BEq Lean.Grind.CommRing.Mon
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.eq_def : ∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory C)
  (x_1 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C x x_1 =
    match x, x_1 with
    | CategoryTheory.FreeMonoidalCategory.of a, x =>
      CategoryTheory.Iso.refl
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
          (CategoryTheory.FreeMonoidalCategory.of a))
    | CategoryTheory.FreeMonoidalCategory.unit, x =>
      CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
    | X.tensor Y, n =>
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusionObj n) X
            Y).symm ≪≫
        CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n)
            Y ≪≫
          CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y (X.normalizeObj n)
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.ofMulDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : Group E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y),
  NormedGroup.ofMulDist' h₁ h₂ =
    { toNorm := (SeminormedGroup.ofMulDist' h₁ h₂).toNorm, toGroup := (SeminormedGroup.ofMulDist' h₁ h₂).toGroup,
      toPseudoMetricSpace := (SeminormedGroup.ofMulDist' h₁ h₂).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }
-- Mathlib.Order.Sublattice
Sublattice.comap_comap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (L : Sublattice γ) (g : LatticeHom β γ) (f : LatticeHom α β),
  Sublattice.comap f (Sublattice.comap g L) = Sublattice.comap (g.comp f) L
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_sumCongr : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (σa : Equiv.Perm α) (σb : Equiv.Perm β), Equiv.Perm.sign (σa.sumCongr σb) = Equiv.Perm.sign σa * Equiv.Perm.sign σb
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_eq_zero_of_le : ∀ {K : Type u_1} [inst : RCLike K] {a : K}, ‖a‖ ≤ RCLike.re a → RCLike.im a = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- `ιK` is a kernel.  -/
CategoryTheory.Triangulated.AbelianSubcategory.isLimitKernelFork : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  {ι : CategoryTheory.Functor A C} →
                    (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
                        n < 0 → f = 0) →
                      {X₁ X₂ : A} →
                        {f₁ : X₁ ⟶ X₂} →
                          {X₃ : C} →
                            {f₂ : ι.obj X₂ ⟶ X₃} →
                              {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)} →
                                (hT :
                                    CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
                                      CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                  {K Q : A} →
                                    {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} →
                                      {β : X₃ ⟶ ι.obj Q} →
                                        {γ :
                                            ι.obj Q ⟶
                                              (CategoryTheory.shiftFunctor C 1).obj
                                                ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))} →
                                          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles →
                                            [inst_7 : ι.Full] →
                                              [inst_8 : CategoryTheory.Preadditive A] →
                                                [inst_9 : ι.Faithful] →
                                                  CategoryTheory.Limits.IsLimit
                                                    (CategoryTheory.Limits.KernelFork.ofι
                                                      (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α) ⋯)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_le : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R}, I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ 1 = 1
-- Init.Data.Nat.Lemmas
Nat.decidableBallLT_eq_decidableBallLTTR : Nat.decidableBallLT = Nat.decidableBallLTTR
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.alts : Lean.Meta.MatcherApp → Array Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The bijection `((sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj F)` which
is part of the universal property of the sheafification of the presheaf of modules `M₀`,
when `F` is a presheaf of modules which is a sheaf.  -/
PresheafOfModules.sheafifyHomEquiv' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          [J.WEqualsLocallyBijective AddCommGrpCat] →
                            {F : PresheafOfModules R.obj} →
                              CategoryTheory.Presheaf.IsSheaf J F.presheaf →
                                ((PresheafOfModules.sheafify α φ).val ⟶ F) ≃
                                  (M₀ ⟶ (PresheafOfModules.restrictScalars α).obj F)
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleRing.assoc_def : ∀ {L : Type u_1} [self : LieAdmissibleRing L] (x y z : L),
  associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_pow : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (x : CentroidHom α) (n : ℕ), (x ^ n).toEnd = x.toEnd ^ n
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.map_setToSimpleFunc : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] [inst_4 : NormedAddCommGroup G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (T : Set α → F →L[ℝ] F'),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f : MeasureTheory.SimpleFunc α G},
      MeasureTheory.Integrable (⇑f) μ →
        ∀ {g : G → F},
          g 0 = 0 →
            MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) =
              ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)],
  Std.DHashMap.Internal.AssocList.getEntry! a Std.DHashMap.Internal.AssocList.nil = default
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation from a metric space is a uniform embedding  -/
Dilation.isUniformEmbedding : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β]
  [inst_2 : PseudoEMetricSpace β] [DilationClass F α β] (f : F), IsUniformEmbedding ⇑f
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] {β : Type w} [inst_1 : Std.Iterator α m β] (it : Std.IterM m β),
  it.toList = Array.toList <$> it.toArray