mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_even_add_odd : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M},
  (Summable fun k => f (2 * k)) →
    (Summable fun k => f (2 * k + 1)) → ∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k
-- Init.Data.Array.MinMax
Array.min_eq_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
  (h : xs ≠ #[]), xs.min h = a ↔ a ∈ xs ∧ ∀ b ∈ xs, a ≤ b
-- Init.Grind.Norm
Int.lt.eq_1 : ∀ (a b : ℤ), a.lt b = (a + 1 ≤ b)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.continuousOn_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ContinuousOn (↑e.symm) e.target
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  0 ≤ x → n ≠ 0 → 0 < ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.Order.SymmDiff
toDual_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α),
  OrderDual.toDual (bihimp a b) = symmDiff (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.eq_of_comp_right_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : Y ⟶ X),
  ((fun {Z} h => CategoryTheory.CategoryStruct.comp h f) = fun {Z} h => CategoryTheory.CategoryStruct.comp h g) → f = g
-- Init.Data.Ord.Basic
lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [DecidableLT α] [DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ (x y : α), x ≤ y ∨ y ≤ x) → (∀ {x y : α}, ¬x ≤ y ↔ y < x) → ∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f]
  [∀ {Z : C} (g h : CategoryTheory.Limits.image f ⟶ Z),
      CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)],
  CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_efixedPoint_lt_top' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤), edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) < ⊤
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_le_of_notMem : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, a ∉ s → (a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The natural isomorphism `A ⊗[S] (S ⊗[R] B) ≃ₐ[T] A ⊗[R] B`.  -/
Algebra.TensorProduct.cancelBaseChange : (R : Type uR) →
  (S : Type uS) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            (A : Type u_4) →
              (B : Type u_5) →
                [inst_3 : CommSemiring T] →
                  [inst_4 : CommSemiring A] →
                    [inst_5 : CommSemiring B] →
                      [inst_6 : Algebra R T] →
                        [inst_7 : Algebra R A] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Algebra T A] →
                              [inst_10 : IsScalarTower R T A] →
                                [inst_11 : Algebra S A] →
                                  [IsScalarTower R S A] →
                                    [inst_13 : Algebra S T] →
                                      [inst_14 : IsScalarTower S T A] →
                                        TensorProduct S A (TensorProduct R S B) ≃ₐ[T] TensorProduct R A B
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_lt_pi_div_two : ∀ {x : ℝ}, Real.arcsin x < Real.pi / 2 ↔ x < 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fourth simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_of_gt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (X.δ i.succ) =
      CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)
-- Init.Data.UInt.Lemmas
USize.neg_eq_neg_one_mul : ∀ (a : USize), -a = -1 * a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {f : β k → β k}, (↑(m.modify k f)).size = (↑m).size
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_zero_pnat_eq_tsum_nat : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {f : ℕ → G}, Summable f → f 0 + ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
-- Mathlib.Analysis.Normed.Module.Basic
instNormedAlgebraULift : (𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    [inst : NormedField 𝕜] → [inst_1 : SeminormedRing 𝕜'] → [NormedAlgebra 𝕜 𝕜'] → NormedAlgebra 𝕜 (ULift.{u_6, u_2} 𝕜')
-- Mathlib.Order.Filter.CountableInter
/-- Construct a filter with countable intersection property.
Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
Similarly to `Filter.ofCountableInter`,
this constructor deduces some properties from the countable intersection property
which becomes the countable union property because we take complements of all sets.  -/
Filter.ofCountableUnion : {α : Type u_2} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) → (∀ t ∈ l, ∀ s ⊆ t, s ∈ l) → Filter α
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C],
  (Φ.transfiniteCompositionOfShapeιIteration J).isColimit = Φ.isColimitIterationCocone J
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor_map_inclRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  {d d' : D} (f : d ⟶ d'),
  (CategoryTheory.Join.mkFunctor F G α).map ((CategoryTheory.Join.inclRight C D).map f) = G.map f
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instModuleComplexOfHasDetOneFinOfNatNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → [Γ.HasDetOne] → Module ℂ (ModularForm Γ k)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The category of groups and group morphisms.  -/
GrpCat : Type (u + 1)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.homInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A), M.homInhabited = { default := M.id }
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.bvar.inj : ∀ {idx idx_1 : ℕ}, Lean.Meta.ArrowPropResult.bvar✝ idx = Lean.Meta.ArrowPropResult.bvar✝ idx_1 → idx = idx_1
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {it : Std.IterM Id α}, it.internalState.next = some a → a ≤ it.internalState.upperBound → it.IsPlausibleOutput a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → Array α → Sort u_2) (xs : Array α) (h_1 : (xs : Array α) → motive 0 xs)
  (h_2 : (n : ℕ) → (xs : Array α) → motive n.succ xs),
  (match 0, xs with
    | 0, xs => h_1 xs
    | n.succ, xs => h_2 n xs) =
    h_1 xs
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_congr_lhs : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} {f : Polynomial R} {r : R}, f.coeff m = r → m = n → f.coeff n = r
-- Init.Data.List.Erase
List.erase_eq_eraseIdx_of_idxOf : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α} {i : ℕ},
  List.idxOf a l = i → l.erase a = l.eraseIdx i
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_fst : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], ⇑(LieHom.fst R L₁ L₂) = Prod.fst
-- Mathlib.Data.Set.Restrict
Set.preimage_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {u : Set ↑t},
  t.restrictPreimage f ⁻¹' u = (fun a => f ↑a) ⁻¹' Subtype.val '' u
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F.leftOp : Jᵒᵖ ⥤ C` into a colimit for `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c) →
              CategoryTheory.Limits.IsColimit c
-- Lean.ToExpr
Lean.instToExprInt8 : Lean.ToExpr Int8
-- Std.Data.String.ToInt
String.toInt?_eq_none : ∀ {s : String}, s.isInt = false → s.toInt? = none
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ)
  {Z : Type u} (h : (f.filtration (Order.succ j)).toSSet.obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.ιSigmaStdSimplex.app x) (CategoryTheory.CategoryStruct.comp ((f.b j).app x) h) =
    CategoryTheory.CategoryStruct.comp (c.mapToSucc.app x) h
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimitsOfSize.eq_1 : CommMonCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.MeasureTheory.Group.Arithmetic
MulOpposite.instMeasurableSpace : {α : Type u_2} → [h : MeasurableSpace α] → MeasurableSpace αᵐᵒᵖ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filter f t) k =
    ((Std.ExtDTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Analysis.SpecificLimits.Basic
Set.Countable.exists_pos_forall_sum_le : ∀ {ι : Type u_4} {s : Set ι},
  s.Countable → ∀ {ε : ℝ}, 0 < ε → ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
-- Plausible.Testable
/-- Hard code the seed to use for the RNG
 -/
Plausible.Configuration.randomSeed : Plausible.Configuration → Option ℕ
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instReprStained.repr : Mathlib.Linter.Flexible.Stained✝ → ℕ → Std.Format
-- Mathlib.Data.ZMod.Basic
ZMod.cast_one' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n], ZMod.cast 1 = 1
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_eq_descFactorialBinary : Nat.descFactorial = Nat.descFactorialBinary
-- Mathlib.GroupTheory.GroupAction.Basic
/-- **Alias** of `AddAction.stabilizer_vadd_eq_stabilizer_map_addConj`.

---

If the stabilizer of `a` is `S`, then the stabilizer of `g +ᵥ a` is `g+S-g`.  -/
AddAction.stabilizer_vadd_eq_stabilizer_map_conj : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  AddAction.stabilizer G (g +ᵥ a) =
    AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) (AddAction.stabilizer G a)
-- Init.Data.Rat.Lemmas
Rat.mul_pos : ∀ {a b : ℚ}, 0 < a → 0 < b → 0 < a * b
-- Mathlib.Algebra.Algebra.Operations
Submodule.le_one_toAddSubmonoid : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A],
  1 ≤ Submodule.toAddSubmonoid 1
-- Mathlib.GroupTheory.DivisibleHull
/-- The divisible hull of an `AddCommMonoid` (as a ℕ-module) is the localized module by
`ℕ+` (implemented using `nonZeroDivisors ℕ`), thus a ℕ-divisible group, or a `ℚ≥0`-module.  -/
DivisibleHull : (M : Type u_1) → [AddCommMonoid M] → Type u_1
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.leftInvOn_piecewise : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y}
  [inst_2 : (i : X) → Decidable (i ∈ s)] [inst_3 : (i : Y) → Decidable (i ∈ t)],
  e.IsImage s t →
    e'.IsImage s t → Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.get! a = m.getD a default
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instCommMonoidWithZero : {α : Type u_1} → [CommMonoidWithZero α] → CommMonoidWithZero αᵒᵈ
-- Mathlib.GroupTheory.Focal
/-- Lemma: The focal subgroup is contained in the commutator subgroup G'.  -/
AddSubgroup.focalAddSubgroup_le_addCommutator : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.focalAddSubgroup ≤ addCommutator G
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.reflectsIsomorphisms_of_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [(F.comp G).ReflectsIsomorphisms],
  F.ReflectsIsomorphisms
-- Init.PropLemmas
/-- Construct a non-Prop by cases on an `Or`, when the right conjunct is decidable.  -/
Or.by_cases' : {q p : Prop} → [Decidable q] → {α : Sort u} → p ∨ q → (p → α) → (q → α) → α
-- Mathlib.Topology.MetricSpace.Gluing
/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
with each factor.
We choose a construction that works for unbounded spaces, but requires basepoints,
chosen arbitrarily.
We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default.  -/
Metric.Sigma.dist : {ι : Type u_1} → {E : ι → Type u_2} → [(i : ι) → MetricSpace (E i)] → (i : ι) × E i → (i : ι) × E i → ℝ
-- Mathlib.Data.Set.Card
Set.encard_union_le : ∀ {α : Type u_1} (s t : Set α), (s ∪ t).encard ≤ s.encard + t.encard
-- Mathlib.Data.Fintype.Basic
Fin.image_castSucc : ∀ (n : ℕ), Finset.image Fin.castSucc Finset.univ = {Fin.last n}ᶜ
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_eq_zero_iff' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {f : α →₀ M},
  Finsupp.subtypeDomain p f = 0 ↔ ∀ (x : α), p x → f x = 0
-- Mathlib.Order.CompleteBooleanAlgebra
sup_iInf₂_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Coframe α] {f : (i : ι) → κ i → α} (a : α),
  a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j
-- Lean.Elab.Tactic.Try
/-- Returns `true` if `tac` is `sorry`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.isSorry : Lean.TSyntax `tactic → Bool
-- Mathlib.Algebra.Opposites
/-- The element of `α` represented by `x : αᵃᵒᵖ`.  -/
AddOpposite.unop : {α : Type u_1} → αᵃᵒᵖ → α
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallHom.shift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y : C}
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  (f f_1 : CategoryTheory.Localization.SmallHom W X Y),
  f = f_1 →
    ∀ (a : M)
      [inst_5 :
        CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X)
          ((CategoryTheory.shiftFunctor C a).obj Y)],
      f.shift a = f_1.shift a
-- Init.Data.UInt.Lemmas
UInt32.toNat_lt_size : ∀ (a : UInt32), a.toNat < UInt32.size
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyLemma.mk.injEq : ∀ (name name_1 : Mathlib.Tactic.ClickSuggestions.Premise), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Init.Data.String.Slice
/-- Splits a slice at each subslice that matches the pattern `pat`.

The subslices that matched the pattern are not included in any of the resulting subslices. If
multiple subslices in a row match the pattern, the resulting list will contain empty strings.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.splitToSubslice Char.isWhitespace).toStringList == ["coffee", "tea", "water"]`

* `("coffee tea water".toSlice.splitToSubslice ' ').toStringList == ["coffee", "tea", "water"]`

* `("coffee tea water".toSlice.splitToSubslice " tea ").toStringList == ["coffee", "water"]`

* `("ababababa".toSlice.splitToSubslice "aba").toStringList == ["coffee", "water"]`

* `("baaab".toSlice.splitToSubslice "aa").toStringList == ["b", "ab"]`
 -/
String.Slice.splitToSubslice : {ρ : Type} →
  {σ : String.Slice → Type} →
    (s : String.Slice) → (pat : ρ) → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → Std.Iter s.Subslice
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [inst_1 : SizeOf A] (carrier : Ideal A)
  (isSubideal : carrier ≤ I) (dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier),
  sizeOf { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem } = 1 + sizeOf carrier
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_iff_singleton : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → (s.Subsingleton ↔ s = {x})
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.Indep.of_isMinor : ∀ {α : Type u_1} {M N : Matroid α} {I : Set α}, N.Indep I → N ≤m M → M.Indep I
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.mk.inj : ∀ {α : Type u_4} {Has : Set α → Prop} {has_empty : Has ∅} {has_compl : ∀ {a : Set α}, Has a → Has aᶜ}
  {has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)}
  {Has_1 : Set α → Prop} {has_empty_1 : Has_1 ∅} {has_compl_1 : ∀ {a : Set α}, Has_1 a → Has_1 aᶜ}
  {has_iUnion_nat_1 :
    ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has_1 (f i)) → Has_1 (⋃ i, f i)},
  { Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } =
      { Has := Has_1, has_empty := has_empty_1, has_compl := has_compl_1, has_iUnion_nat := has_iUnion_nat_1 } →
    Has = Has_1
-- Mathlib.Data.Set.Function
Set.injOn_insert : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {a : α},
  a ∉ s → (Set.InjOn f (insert a s) ↔ Set.InjOn f s ∧ f a ∉ f '' s)
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, the natural hom sending `y : M`, `M` an `AddCommMonoid`, to the equivalence
class of `(y, 0)` in the Localization of `M` at the Submonoid generated by `x`.  -/
AddLocalization.Away.addMonoidOf : {M : Type u_1} → [inst : AddCommMonoid M] → (x : M) → AddSubmonoid.LocalizationMap.AwayMap x (AddLocalization.Away x)
-- LeanSearchClient.Syntax
LeanSearchClient.stateSearchTacticImpl : Lean.Elab.Tactic.Tactic
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.Order.Monotone.Defs
Subtype.mono_coe : ∀ {α : Type u} [inst : Preorder α] (p : α → Prop), Monotone Subtype.val
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.isEq_compare_eq_beq : ∀ {α : Type u} {x : Ord α} {x_1 : BEq α} [Std.LawfulBEqOrd α] {a b : α}, (compare a b).isEq = (a == b)
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_intCast_ite : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ} {a : ℤ}, (↑a).coeff n = ↑(if n = 0 then a else 0)
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint over `F` and one of them is algebraic,
then `A ⊗[F] L` is a field.  -/
IntermediateField.LinearDisjoint.isField_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L → Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L → IsField (TensorProduct F (↥A) L)
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.addRuleFailure : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.RegularRule → Aesop.GoalRef → Aesop.SearchM Q Unit
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f] [IrreducibleSpace ↥S],
  IsOpenMap ⇑f → IrreducibleSpace ↥X
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.instNonemptyOctahedron : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C] (X : C),
  Nonempty (CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯)
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.polarCoord_source : Complex.polarCoord.source = Complex.slitPlane
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_hom_comp_f_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 A).f)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesIso₀ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) (groupCohomology.cochainsIso₀ A).hom))
      x
-- Init.Data.Nat.Lemmas
Nat.self_add_pred : ∀ (n : ℕ), n + n.pred = (2 * n).pred