mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
Array.getElem?_empty : ∀ {α : Type u_1} {i : ℕ}, #[][i]? = none
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.as.sizeOf_spec : ∀ (varId : Lean.FVarId) (p : Lean.Meta.Match.Pattern) (hId : Lean.FVarId),
  sizeOf (Lean.Meta.Match.Pattern.as varId p hId) = 1 + sizeOf varId + sizeOf p + sizeOf hId
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.sign.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (h_1 : (n : ℕ) → motive (Int.ofNat n.succ)) (h_2 : Unit → motive (Int.ofNat 0))
  (h_3 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.ofNat 0 with
    | Int.ofNat n.succ => h_1 n
    | Int.ofNat 0 => h_2 ()
    | Int.negSucc a => h_3 a) =
    h_2 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.strictAntiOn_cos : StrictAntiOn Real.cos (Set.Icc 0 Real.pi)
-- Mathlib.Analysis.Normed.Group.Quotient
AddSubgroup.quotientIsometryEquivOfEq.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S T : AddSubgroup M} (h : S = T),
  AddSubgroup.quotientIsometryEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, isometry_toFun := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_refl : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], (AffineEquiv.refl k P₁).linear = LinearEquiv.refl k V₁
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.one_mem_range_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), 1 ∈ Set.range fun p => ∑ i, a i * b i ^ p
-- Init.Tactics
/-- `massumption` is like `assumption`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
  mintro _ _
  massumption
```
 -/
Lean.Parser.Tactic.massumptionMacro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Pi
/-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
and colimits exist for each of the `F ⋙ Pi.eval C i`,
there is a colimit for `F`.
 -/
CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval : ∀ {I : Type v₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type v₁}
  [inst_1 : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)}
  [∀ (i : I), CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Pi.eval C i))],
  CategoryTheory.Limits.HasColimit F
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_insertMany_list_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {l : List α} {k : α}, k ∈ m → (m.insertMany l).get! k = m.get! k
-- Init.Data.SInt.Basic
/-- Bitwise and for 64-bit signed integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set,
according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.land : Int64 → Int64 → Int64
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_genWeightSpace_eq : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [IsDomain R] [IsPrincipalIdealRing R] [inst_10 : LieRing.IsNilpotent L] [IsNoetherian R M]
  [LieModule.LinearWeights R L M] (χ : L → R) (x y : L),
  ((LieModule.traceForm R L ↥(LieModule.genWeightSpace M χ)) x) y =
    Module.finrank R ↥(LieModule.genWeightSpace M χ) • (χ x * χ y)
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_same : ∀ {b : ByteArray} {i : ℕ}, b.extract i i = ByteArray.empty
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getOptRotation : Lean.Syntax → ℕ
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.eq : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.IsSymm → A.transpose = A
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.lhs : Nat.Internal.Linear.ExprCnstr → Nat.Internal.Linear.Expr
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_of : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A) (x : G),
  ((SkewMonoidAlgebra.lift k G A) F) ((SkewMonoidAlgebra.of k G) x) = F x
-- Mathlib.RingTheory.PowerSeries.Order
/-- Dividing `X` by the maximal power of `X` dividing it leaves `1`.  -/
PowerSeries.divXPowOrder_X : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], PowerSeries.X.divXPowOrder = 1
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_eq_tsum : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] [CharZero 𝕂], NormedSpace.exp = fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_prod : ∀ {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [inst : CommMonoid β] {f : ι → α → β} (I : Finset ι),
  (UniformOnFun.toFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (UniformOnFun.toFun 𝔖) (f i)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mk'.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (functor_unitIso_comp :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) =
          CategoryTheory.CategoryStruct.id (functor.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam)
  (functor_1 : CategoryTheory.Functor C D) (inverse_1 : CategoryTheory.Functor D C)
  (unitIso_1 : CategoryTheory.Functor.id C ≅ functor_1.comp inverse_1)
  (counitIso_1 : inverse_1.comp functor_1 ≅ CategoryTheory.Functor.id D)
  (functor_unitIso_comp_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor_1.map (unitIso_1.hom.app X))
            (counitIso_1.hom.app (functor_1.obj X)) =
          CategoryTheory.CategoryStruct.id (functor_1.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam),
  ({ functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
        functor_unitIso_comp := functor_unitIso_comp } =
      { functor := functor_1, inverse := inverse_1, unitIso := unitIso_1, counitIso := counitIso_1,
        functor_unitIso_comp := functor_unitIso_comp_1 }) =
    (functor = functor_1 ∧ inverse = inverse_1 ∧ unitIso ≍ unitIso_1 ∧ counitIso ≍ counitIso_1)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.add_mem_sup : ∀ {G : Type u_1} [inst : AddGroup G] {S T : AddSubgroup G} {x y : G}, x ∈ S → y ∈ T → x + y ∈ S ⊔ T
-- Mathlib.Dynamics.Ergodic.Action.Basic
MeasureTheory.aeconst_of_forall_smul_ae_eq : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Group G]
  [inst_1 : MulAction G α] [ErgodicSMul G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (∀ (g : G), g • s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_comp_substAlgHom_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {υ : Type u_7} {T : Type u_8} [inst_3 : CommRing T]
  [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {b : τ → MvPowerSeries υ T}
  (ha : MvPowerSeries.HasSubst a) (hb : MvPowerSeries.HasSubst b) (f : MvPowerSeries σ R),
  (MvPowerSeries.substAlgHom hb) ((MvPowerSeries.substAlgHom ha) f) = (MvPowerSeries.substAlgHom ⋯) f
-- Aesop.RuleTac.Basic
Aesop.RuleTacOutput.mk.sizeOf_spec : ∀ (applications : Array Aesop.RuleApplication), sizeOf { applications := applications } = 1 + sizeOf applications
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The single functor `C ⥤ HomotopyCategory.Plus C`.  -/
HomotopyCategory.Plus.singleFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → ℤ → CategoryTheory.Functor C (HomotopyCategory.Plus C)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G} {x : G}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Order.Filter.IndicatorFunction
indicator_eventuallyLE_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {l : Filter α},
  f ≤ᶠ[l ⊓ Filter.principal s] g → s.indicator f ≤ᶠ[l] s.indicator g
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_cons_reduce : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α] (a : α × Bool),
  FreeGroup.reduce (a :: FreeGroup.reduce L) = FreeGroup.reduce (a :: L)
-- Mathlib.SetTheory.Lists
Lists.mem.decidable.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : Lists α) (x_1 : Lists' α true),
  Lists.mem.decidable x x_1 =
    match x, x_1 with
    | a, Lists'.nil => isFalse ⋯
    | a, b_1.cons' l₂ => decidable_of_iff' (a.Equiv ⟨b, b_1⟩ ∨ a ∈ l₂) ⋯
-- Mathlib.RingTheory.Perfection
ModP.v_p_lt_preVal : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ {p : ℕ} {x : ModP O p}, v ↑p < ModP.preVal K v O p x ↔ x ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_lt_rpow_iff_of_pos : ∀ {x y : ℝ}, 0 < x → (1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.continuous_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero R],
  Continuous TrivSqZeroExt.inr
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- Sometimes rewriting with `comp_c_app` doesn't work because of dependent type issues.
In that case, `erw comp_c_app_assoc` might make progress.
The lemma `comp_c_app_assoc` is also better suited for rewrites in the opposite direction.  -/
AlgebraicGeometry.PresheafedSpace.comp_c_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y)
  (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ),
  (CategoryTheory.CategoryStruct.comp α β).c.app U =
    CategoryTheory.CategoryStruct.comp (β.c.app U)
      (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U))))
-- Mathlib.Algebra.Torsor.Defs
vadd_vsub_vadd_cancel_right : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (v₁ v₂ : G) (p : P),
  (v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) = v₁ - v₂
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.matched.sizeOf_spec : ∀ {s : String.Slice} (startPos endPos : s.Pos),
  sizeOf (String.Slice.Pattern.SearchStep.matched startPos endPos) = 1 + sizeOf startPos + sizeOf endPos
-- Mathlib.Probability.Distributions.Exponential
/-- The exponential pdf is measurable.  -/
ProbabilityTheory.measurable_exponentialPDFReal : ∀ (r : ℝ), Measurable (ProbabilityTheory.exponentialPDFReal r)
-- Mathlib.Tactic.Linarith.Preprocessing
/-- **Alias** of `Mathlib.Tactic.Linarith.mkNonstrictIntProof?`.

---

If `pf` is a proof of a strict inequality `(a : ℤ) < b`,
`mkNonstrictIntProof pf` returns a proof of `a + 1 ≤ b`,
and similarly if `pf` proves a negated weak inequality.
 -/
Mathlib.Tactic.Linarith.mkNonstrictIntProof : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.XIsoBiprod.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j)
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)],
  HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij = CategoryTheory.eqToIso ⋯
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coneOfPreserves_pt_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R]
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)))
  {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂),
  (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.hom =
    (CategoryTheory.Limits.isLimitOfPreserves R t₂).lift (CategoryTheory.Comma.limitAuxiliaryCone F c₁)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Predicate asserting that the word `L` is cyclically reduced, i.e., it is reduced and furthermore
the first and the last letter of the word do not cancel. The empty word is by convention also
cyclically reduced.  -/
FreeGroup.IsCyclicallyReduced : {α : Type u} → List (α × Bool) → Prop
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R} (h : I ≤ J),
  (↑(DoubleQuot.quotQuotEquivQuotOfLE h)).comp (DoubleQuot.quotQuotMk I J) = Ideal.Quotient.mk J
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Differentiable.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.exp (f x)
-- Mathlib.Analysis.RCLike.Basic
/-- The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when `RCLike.I = 0`.  -/
RCLike.realRingEquiv : {K : Type u_1} → [inst : RCLike K] → RCLike.I = 0 → K ≃+* ℝ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) [SecondCountableTopology X]
  {ρ : MeasureTheory.Measure X}, ρ.AbsolutelyContinuous μ → ρ s ≤ ∑' (p : ↑h.index), ρ (h.covering ↑p)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note this is more general for matrices than `isSelfAdjoint_one` as it does not
require `Fintype n`, which is necessary for `Monoid (Matrix n n R)`.  -/
Matrix.isHermitian_one : ∀ {α : Type u_1} {n : Type u_4} [inst : NonAssocSemiring α] [inst_1 : StarRing α] [inst_2 : DecidableEq n],
  Matrix.IsHermitian 1
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- If `S` is a von Neumann bounded set of continuous linear maps `f : E →SL[σ] F`
and `s` is a von Neumann bounded set in the domain,
then the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.

See also `isVonNBounded_iff` for an `Iff` version with stronger typeclass assumptions.  -/
ContinuousLinearMap.isVonNBounded_image2_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] {R : Type u_7} [inst_7 : SeminormedRing R] [inst_8 : TopologicalSpace F]
  [inst_9 : IsTopologicalAddGroup F] [inst_10 : DistribMulAction R F] [inst_11 : ContinuousConstSMul R F]
  [inst_12 : SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)},
  Bornology.IsVonNBounded R S →
    ∀ {s : Set E}, Bornology.IsVonNBounded 𝕜₁ s → Bornology.IsVonNBounded R (Set.image2 (fun f x => f x) S s)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.ne_self_add_add_utf8Size : ∀ {i n : ℕ} {c : Char}, i ≠ i + (n + c.utf8Size)
-- Mathlib.Order.Interval.Set.Image
StrictAnti.mapsTo_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.lintegral_comp_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ ν →
    MeasurableEmbedding g → ∀ (f : β → ENNReal), ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Finset.Ici a = LocallyFiniteOrderTop.finsetIci a
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
/-- `EReal.exp` and its inverse `ENNReal.log` are an order isomorphism between `EReal` and
`ℝ≥0∞`.  -/
EReal.expOrderIso : EReal ≃o ENNReal
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCones_pt_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂),
  (CategoryTheory.Limits.combineCones F c).pt.map f =
    (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone.π (F.flip.map f) }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs c_1 →
    c = c_1
-- Mathlib.Order.Closure
LowerAdjoint.ext : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l₁ l₂ : LowerAdjoint u),
  l₁.toFun = l₂.toFun → l₁ = l₂
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sbtw_touchpoint_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Sbtw ℝ (t.points i₁) (Affine.Simplex.touchpoint t {i₂} i₂) (t.points i₃)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.instPartialOrder : {X : SSet} → {A : X.Subcomplex} → PartialOrder A.N
-- Mathlib.Topology.Order
continuous_top : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α}, Continuous f
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.nontrivial : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), 0 ∉ S → Nontrivial N
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  [CategoryTheory.IsIso φ], CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.OplaxLinear C` equips `F : D ⥤ D'` with a family of morphisms
`δₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d)`
that is natural in each variable and coherent with respect to left actions
of `C` on `D` and `D'`.  -/
CategoryTheory.Functor.OplaxLeftLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] → Type (max (max u_1 u_3) v_2)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.StrongCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (η.app b))
  (naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom._autoParam),
  sizeOf { naturality := naturality, naturality_hom := naturality_hom } = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJEqZeroNF.a₁ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharTwoJEqZeroNF], W.a₁ = 0
-- Mathlib.GroupTheory.GroupAction.Basic
/-- The natural group equivalence between the stabilizers of two elements in the same orbit.  -/
MulAction.stabilizerEquivStabilizer : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {g : G} → {a b : α} → b = g • a → ↥(MulAction.stabilizer G a) ≃* ↥(MulAction.stabilizer G b)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.mk.inj : ∀ {C : Type u_1} {ι : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} ι} {inst_2 : CategoryTheory.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.HasShift C ℤ} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {hom : X.ω₁ ⟶ Y.ω₁}
  {comm :
    autoParam
      (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g)
            ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
          CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
      CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam}
  {hom_1 : X.ω₁ ⟶ Y.ω₁}
  {comm_1 :
    autoParam
      (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g)
            ((CategoryTheory.shiftFunctor C 1).map (hom_1.app (CategoryTheory.ComposableArrows.mk₁ f))) =
          CategoryTheory.CategoryStruct.comp (hom_1.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
      CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.whiskerRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z : C) →
        [CategoryTheory.MonoidalCoherence X Y] →
          CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)