mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.map_zsmul' : ∀ {M : Type u_4} {N : Type u_5} [inst : SubNegMonoid M] [inst_1 : SubNegMonoid N] (f : M →+ N),
  (∀ (x : M), f (-x) = -f x) → ∀ (n : ℤ) (a : M), f (n • a) = n • f a
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocDiv hp (a + OfNat.ofNat m * p) b = toIocDiv hp a b - OfNat.ofNat m
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`.  -/
AddAction.set_mem_fixedBy_of_movedBy_subset : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {g : G},
  (AddAction.fixedBy α g)ᶜ ⊆ s → s ∈ AddAction.fixedBy (Set α) g
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
rieszContent.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  (Λ Λ_1 : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal), Λ = Λ_1 → rieszContent Λ = rieszContent Λ_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_eq_zero_of_subsingleton : ∀ {V : Type u_1} {G : SimpleGraph V} (v : V) [inst : Fintype ↑(G.neighborSet v)] [Subsingleton V], G.degree v = 0
-- Mathlib.RingTheory.Etale.Basic
RingHom.FormallyEtale.comp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.FormallyEtale → g.FormallyEtale → (g.comp f).FormallyEtale
-- Lean.Elab.Command
Lean.Elab.Command.Context.mk.sizeOf_spec : ∀ (fileName : String) (fileMap : Lean.FileMap) (currRecDepth : ℕ) (cmdPos : String.Pos.Raw)
  (macroStack : Lean.Elab.MacroStack) (quotContext? : Option Lean.Name) (currMacroScope : Lean.MacroScope)
  (ref : Lean.Syntax) (snap? : Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot))
  (cancelTk? : Option IO.CancelToken) (suppressElabErrors : Bool),
  sizeOf
      { fileName := fileName, fileMap := fileMap, currRecDepth := currRecDepth, cmdPos := cmdPos,
        macroStack := macroStack, quotContext? := quotContext?, currMacroScope := currMacroScope, ref := ref,
        snap? := snap?, cancelTk? := cancelTk?, suppressElabErrors := suppressElabErrors } =
    1 + sizeOf fileName + sizeOf fileMap + sizeOf currRecDepth + sizeOf cmdPos + sizeOf macroStack +
                sizeOf quotContext? +
              sizeOf currMacroScope +
            sizeOf ref +
          sizeOf snap? +
        sizeOf cancelTk? +
      sizeOf suppressElabErrors
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.FinitaryExtensive C],
  CategoryTheory.FinitaryExtensive (CategoryTheory.Functor D C)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.splitEpi_g_section_ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), s.splitEpi_g.section_ = s.s
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.tagAppFns : Lean.Option Bool
-- Mathlib.LinearAlgebra.Dimension.Basic
nonempty_linearIndependent_set : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Nonempty { s // LinearIndepOn R id s }
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], MeasureTheory.Measure.snd 0 = 0
-- Mathlib.Data.List.GetD
List.getI_nil : ∀ {α : Type u} (n : ℕ) [inst : Inhabited α], [].getI n = default
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.desc_comp_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N), h.desc s ∘ₗ solution.π = s.π
-- Init.Data.String.Defs
String.Slice.byteIdx_rawEndPos : ∀ {s : String.Slice}, s.rawEndPos.byteIdx = s.utf8ByteSize
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl_apply : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] (A : Matrix V V α) [inst_2 : Zero α]
  [inst_3 : One α] (i j : V), A.compl i j = 0 ∨ A.compl i j = 1
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split_eq_next_of_not_matchesAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {firstRejected start : s.Pos}
  {hle : firstRejected ≤ start} (hs : start ≠ s.endPos),
  ¬String.Slice.Pattern.Model.MatchesAt pat start →
    String.Slice.Pattern.Model.split pat firstRejected start hle =
      String.Slice.Pattern.Model.split pat firstRejected (start.next hs) ⋯
-- Mathlib.SetTheory.Cardinal.Finite
Function.Injective.bijective_of_nat_card_le : ∀ {α : Type u_1} {β : Type u_2} [Finite β] {f : α → β},
  Function.Injective f → Nat.card β ≤ Nat.card α → Function.Bijective f
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The rank of `(ι →₀ R)` is `(#ι).lift`.  -/
rank_finsupp_self : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (ι : Type w),
  Module.rank R (ι →₀ R) = Cardinal.lift.{u, w} (Cardinal.mk ι)
-- Mathlib.RingTheory.IsTensorProduct
/-- If `S' = S ⊗[R] R'`, then any pair of `R`-algebra homomorphisms `f : S → A` and `g : R' → A`
such that `f x` and `g y` commutes for all `x, y` descends to a (unique) homomorphism `S' → A`.
 -/
Algebra.pushoutDesc : {R : Type u_1} →
  {S : Type v₃} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {R' : Type u_6} →
            (S' : Type u_7) →
              [inst_3 : CommSemiring R'] →
                [inst_4 : CommSemiring S'] →
                  [inst_5 : Algebra R R'] →
                    [inst_6 : Algebra S S'] →
                      [inst_7 : Algebra R' S'] →
                        [inst_8 : Algebra R S'] →
                          [inst_9 : IsScalarTower R R' S'] →
                            [inst_10 : IsScalarTower R S S'] →
                              [H : Algebra.IsPushout R S R' S'] →
                                {A : Type u_8} →
                                  [inst_11 : Semiring A] →
                                    [inst_12 : Algebra R A] →
                                      (f : S →ₐ[R] A) →
                                        (g : R' →ₐ[R] A) → (∀ (x : S) (y : R'), f x * g y = g y * f x) → S' →ₐ[R] A
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.EventuallyEq.of_forall_separating_mem_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → β} (p : Set β → Prop)
  [HasCountableSeparatingOn β p Set.univ], (∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U) → f =ᶠ[l] g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.id_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  (CategoryTheory.ShortComplex.HomologyMapData.id h).left = CategoryTheory.ShortComplex.LeftHomologyMapData.id h.left
-- Mathlib.Data.ENat.Basic
ENat.pow_eq_top_iff : ∀ {a : ℕ∞} {n : ℕ}, a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.tdiv.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_3 m n
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : G →* N},
  Subgroup.map f H = ⊥ ↔ H ≤ f.ker
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_edist_of_le_infsep : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ} {x : α},
  x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → d ≤ s.infsep → d ≤ dist x y
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x₁ x₂ : M} {y₁ y₂ : ↥S},
  f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor reflects effective epimorphic families if families that are mapped to effective
epimorphic families are themselves effective epimorphic families.
 -/
CategoryTheory.Functor.ReflectsEffectiveEpiFamilies.reflects : ∀ {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} {F : CategoryTheory.Functor C D}
  [self : F.ReflectsEffectiveEpiFamilies] {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
  (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonAddHom : ∀ {α : Type u_2} [inst : Add α], ⇑Set.singletonAddHom = singleton
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_mul_cos_add_sin_mul_I : ∀ (x : ℂ), ↑‖x‖ * (Complex.cos ↑x.arg + Complex.sin ↑x.arg * Complex.I) = x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_trans_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₃), (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(yoneda.obj X).obj Y = unop Y ⟶ X`.  -/
CategoryTheory.yoneda_obj_obj_eq_hom' : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → Cᵒᵖ → Cᵒᵖ → Prop
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearAddRight.eq_1 : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  Homeomorph.shearAddRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.addLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k] (r : k) {g g' : G}
  (x : SkewMonoidAlgebra k G), (¬∃ d, g' = g * d) → (SkewMonoidAlgebra.single g r * x).coeff g' = 0
-- Init.Data.BitVec.Lemmas
BitVec.and_cast : ∀ {w w' : ℕ} {x y : BitVec w} (h : w = w'), BitVec.cast h x &&& BitVec.cast h y = BitVec.cast h (x &&& y)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A monoidal category acts on itself through the tensor product.  -/
CategoryTheory.MonoidalCategory.selRightfAction : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory.MonoidalRightAction C C
-- Mathlib.Algebra.Lie.UniversalEnveloping
_private.Mathlib.Algebra.Lie.UniversalEnveloping.0.termιₜ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α],
  OrderDual.instAddCommMonoid = { toAddMonoid := OrderDual.instAddMonoid, add_comm := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.Δ_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2],
  W.Δ = W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3
-- Mathlib.Tactic.NthRewrite
/-- `nth_rewrite` is a variant of `rewrite` that only changes the `n₁, ..., nₖ`ᵗʰ _occurrence_ of
the expression to be rewritten. `nth_rewrite n₁ ... nₖ [eq₁, eq₂,..., eqₘ]` will rewrite the
`n₁, ..., nₖ`ᵗʰ _occurrence_ of each of the `m` equalities `eqᵢ`in that order. Occurrences are
counted beginning with `1` in order of precedence.

For example,
```lean
example (h : a = 1) : a + a + a + a + a = 5 := by
  nth_rewrite 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/
```
Notice that the second and third occurrences of `a` from the left have been rewritten by
`nth_rewrite`.

To understand the importance of order of precedence, consider the example below
```lean
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
  nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c
```
Here, although the occurrence parameter is `2`, `(a + b)` is rewritten to `(b + a)`. This happens
because in order of precedence, the first occurrence of `_ + _` is the one that adds `a + b` to `c`.
The occurrence in `a + b` counts as the second occurrence.

If a term `t` is introduced by rewriting with `eqᵢ`, then this instance of `t` will be counted as an
_occurrence_ of `t` for all subsequent rewrites of `t` with `eqⱼ` for `j > i`. This behaviour is
illustrated by the example below
```lean
example (h : a = a + b) : a + a + a + a + a = 0 := by
  nth_rewrite 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/
```
Here, the first `nth_rewrite` with `h` introduces an additional occurrence of `a` in the goal.
That is, the goal state after the first rewrite looks like below
```lean
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/
```
This new instance of `a` also turns out to be the third _occurrence_ of `a`.  Therefore,
the next `nth_rewrite` with `h` rewrites this `a`.
 -/
Mathlib.Tactic.tacticNth_rewrite_____ : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.continuous_integral_integral_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E],
  Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a
-- Mathlib.Tactic.Ring.Compare
/-- **Alias** of `Mathlib.Tactic.Ring.addMonoidWithOneOfCommSemiring`.

---

`CommSemiring` implies `AddMonoidWithOne`.  -/
Mathlib.Tactic.Ring.amwo_of_cs : (α : Type u_1) → [CommSemiring α] → AddMonoidWithOne α
-- Mathlib.CategoryTheory.LiftingProperties.Basic
/-- Unique field expressing that any commutative square built from `f` and `g` has a lift  -/
CategoryTheory.HasLiftingProperty.sq_hasLift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y}
  [self : CategoryTheory.HasLiftingProperty i p] {f : A ⟶ X} {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g),
  sq.HasLift
-- Mathlib.Algebra.Group.Indicator
Set.indicator_add_compl_eq_piecewise : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {s : Set α} [inst_1 : DecidablePred fun x => x ∈ s]
  (f g : α → M), s.indicator f + sᶜ.indicator g = s.piecewise f g
-- Init.SimpLemmas
eq_true : ∀ {p : Prop}, p → p = True
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mem_iInf : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {ι : Sort u_1} {p : ι → SubMulAction R M} {x : M},
  x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
-- Lean.Parser.Term
Lean.Parser.Term.let_tmp.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c)
  (U : TopologicalSpace.Opens ↑X) (hU : p₀ ∈ U),
  CategoryTheory.CategoryStruct.comp (𝓕.germ U p₀ hU) (StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ f) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.eqToHom ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {v : β k}, (t.getThenInsertIfNew?! k v).1 = t.get? k
-- Std.Do.Triple.Basic
Std.Do.Triple.entails_wp_of_pre : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α}
  {P P' : Std.Do.Assertion ps} {Q : Std.Do.PostCond α ps}, ⦃P'⦄ x ⦃Q⦄ → (P ⊢ₛ P') → P ⊢ₛ (Std.Do.wp x).apply Q
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDFReal.eq_1 : ∀ (x₀ : ℝ) (γ : NNReal) (x : ℝ), ProbabilityTheory.cauchyPDFReal x₀ γ x = Real.pi⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.oadd : ∀ {e a : ONote}, e.NF → ∀ (n : ℕ+), a.NFBelow e.repr → (e.oadd n a).NF
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond α ps} [inst : Pure m]
  [inst_1 : Std.Do.WP m ps] (x : stM m m α), (Std.Do.wp (restoreM x)).apply Q = (Std.Do.wp (pure x)).apply Q
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A shorthand for `toBiconeFunctor.obj`  -/
CategoryTheory.Limits.BinaryBicone.toBicone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Limits.BinaryBicone X Y → CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)
-- Mathlib.Data.Nat.Nth
Nat.nth_lt_of_lt_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n k : ℕ}, k < Nat.count p n → Nat.nth p k < n
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_mul_right' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b c : α),
  Associated (gcd (b * a) (c * a)) (gcd b c * a)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G},
  Subgroup.IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
-- Mathlib.Data.Set.Prod
Set.prod_range_range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ},
  Set.range m₁ ×ˢ Set.range m₂ = Set.range fun p => (m₁ p.1, m₂ p.2)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right.  -/
vectorSpan_eq_span_vsub_set_right : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P}, p ∈ s → vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' s)
-- Mathlib.Data.Prod.Lex
Prod.Lex.orderTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β], Prod.Lex.orderTop = { top := toLex ⊤, le_top := ⋯ }
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.leftFun_implicitFunction_eq_leftFun : ∀ {𝕜 : 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),
  ∀ᶠ (x : E) in nhds φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inl_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N], Function.Injective ⇑AddMonoid.Coprod.inl
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.pre_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) {X Y : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)}
  (f : X ⟶ Y), ((CategoryTheory.CostructuredArrow.pre F G S).map f).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map_iso_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [Quiver.IsThin C] {F₁ F₂ : CategoryTheory.Functor D C} (h : F₁ ≅ F₂),
  CategoryTheory.ThinSkeleton.map F₁ = CategoryTheory.ThinSkeleton.map F₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_empty : ∀ {α : Type u} {β : Type v}, ∅.keys = []
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.instFormallyUnramifiedResidueField : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : IsLocalRing S], Algebra.FormallyUnramified S (IsLocalRing.ResidueField S)
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
/-- A root system is determined by its Cartan matrix.  -/
RootPairing.Base.equivOfCartanMatrixEq : {ι : 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] →
                  [CharZero R] →
                    [IsDomain R] →
                      [Finite ι] →
                        {ι₂ : Type u_6} →
                          {M₂ : Type u_7} →
                            {N₂ : Type u_8} →
                              [inst_8 : AddCommGroup M₂] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : AddCommGroup N₂] →
                                    [inst_11 : Module R N₂] →
                                      {P : RootPairing ι R M N} →
                                        [P.IsRootSystem] →
                                          [inst_13 : P.IsCrystallographic] →
                                            [P.IsReduced] →
                                              (b : P.Base) →
                                                {P₂ : RootPairing ι₂ R M₂ N₂} →
                                                  [inst_15 : P₂.IsCrystallographic] →
                                                    (b₂ : P₂.Base) →
                                                      (e : ↥b.support ≃ ↥b₂.support) →
                                                        [Finite ι₂] →
                                                          [P₂.IsRootSystem] →
                                                            [P₂.IsReduced] →
                                                              (∀ (i j : ↥b.support),
                                                                  b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) →
                                                                P.Equiv P₂
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_hom_comp_i_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH1 A).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom h)
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.unique : {α : Type u_3} → {E : α → Type u_4} → [inst : (i : α) → NormedAddCommGroup (E i)] → [IsEmpty α] → Unique (PreLp E)