mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).contains k = true
-- Init.Data.Order.Ord
Std.OrientedCmp.not_isLE_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.lt → ¬(cmp b a).isLE = true
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.instSetLike : {R : Type u} → [inst : NonAssocSemiring R] → SetLike (Subsemiring R) R
-- Mathlib.Data.DFinsupp.BigOperators
/-- When summing over an `AddMonoidHom`, the decidability assumption is not needed, and the result is
also an `AddMonoidHom`.
 -/
DFinsupp.sumAddHom : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → AddZeroClass (β i)] →
          [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.cons.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.ForEachM : {ω : Type} → (m : Type → Type) → [STWorld ω m] → Type → Type
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.pow_eq_pow_iff_modEq : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {x : G} {m n : ℕ}, x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_roo : ∀ {m n : ℕ}, (m<...n).toList.toArray = (m<...n).toArray
-- Mathlib.Analysis.Matrix.LDL
LDL.lowerInv_eq_gramSchmidtBasis : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef),
  LDL.lowerInv hS = ((Pi.basisFun 𝕜 n).toMatrix ⇑(InnerProductSpace.gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_sub_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (x - t)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.LinearAlgebra.Determinant
AlternatingMap.map_basis_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [Finite ι] (e : Module.Basis ι R M) (f : M [⋀^ι]→ₗ[R] R), f ⇑e = 0 ↔ f = 0
-- Mathlib.Topology.LocallyFinsupp.Pushforward
Function.locallyFinsupp.map.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (w : X → R) [inst_2 : Semiring R] [inst_3 : PrespectralSpace Y] (hf : IsSpectralMap f)
  (c : Function.locallyFinsupp X R),
  Function.locallyFinsupp.map f w hf c =
    { toFun := fun z => ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x, supportWithinDomain' := ⋯,
      supportLocallyFiniteWithinDomain' := ⋯ }
-- Init.Data.String.Defs
/-- Criterion for validity of positions in string slices.  -/
String.Pos.Raw.IsValidForSlice : String.Slice → String.Pos.Raw → Prop
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_8 : HAdd Std.Time.Millisecond.Offset Std.Time.Minute.Offset Std.Time.Millisecond.Offset
-- Mathlib.Order.Filter.Pointwise
Filter.map_neg' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f : Filter α}, Filter.map (⇑m) (-f) = -Filter.map (⇑m) f
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] {G : SimpleGraph α} {a b : α} (p p_1 : G.Walk a b),
  p = p_1 → p.IsHamiltonian = p_1.IsHamiltonian
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_le : Nat.Internal.Linear.Context → Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly → Prop
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrixAux`.

---

The linear map from bilinear forms to `Matrix n n R` given an `n`-indexed basis.

This is an auxiliary definition for the equivalence `Matrix.toBilin'`.  -/
BilinForm.toMatrixAux : {R₁ : Type u_1} →
  {M₁ : Type u_2} →
    [inst : CommSemiring R₁] →
      [inst_1 : AddCommMonoid M₁] →
        [inst_2 : Module R₁ M₁] → {n : Type u_5} → (n → M₁) → LinearMap.BilinForm R₁ M₁ →ₗ[R₁] Matrix n n R₁
-- Init.Data.Array.Find
Array.find?_eq_bind_findIdx?_getElem? : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.find? p xs = (Array.findIdx? p xs).bind fun x => xs[x]?
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_map : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E}
  {g : α → F} {k : β → α} {l : Filter β},
  Asymptotics.IsBigOWith c (Filter.map k l) f g ↔ Asymptotics.IsBigOWith c l (f ∘ k) (g ∘ k)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.insert_indep_of_indep : ∀ {α : Type u_1} {M : Matroid α} {e : α} {I : Set α}, M.IsColoop e → M.Indep I → M.Indep (insert e I)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
AddSubmonoidClass.finsuppSum_mem : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {S : Type u_16}
  [inst_2 : SetLike S N] [AddSubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N),
  (∀ (c : α), f c ≠ 0 → g c (f c) ∈ s) → f.sum g ∈ s
-- Mathlib.CategoryTheory.Shift.CommShift
/-- For any functor `F : C ⥤ D`, this is the obvious isomorphism
`shiftFunctor C (0 : A) ⋙ F ≅ F ⋙ shiftFunctor D (0 : A)` deduced from the
isomorphisms `shiftFunctorZero` on both categories `C` and `D`.  -/
CategoryTheory.Functor.CommShift.isoZero : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (F : CategoryTheory.Functor C D) →
          (A : Type u_4) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  (CategoryTheory.shiftFunctor C 0).comp F ≅ F.comp (CategoryTheory.shiftFunctor D 0)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_rescale : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (f : MvPowerSeries σ R) (a b : σ → R),
  (MvPowerSeries.rescale b) ((MvPowerSeries.rescale a) f) = (MvPowerSeries.rescale (a * b)) f
-- Mathlib.Order.SuccPred.Archimedean
StrictAnti.not_bddBelow_range_of_isPredArchimedean : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMaxOrder α]
  [inst_4 : PredOrder β] [IsPredArchimedean β], StrictAnti f → ¬BddBelow (Set.range f)
-- Mathlib.Algebra.Group.Units.Basic
Units.eq_inv_of_mul_eq_one_right : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, a * ↑u = 1 → a = ↑u⁻¹
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z : C} {P Q : CategoryTheory.Subobject Y} (f : Z ⟶ Y),
  P ≤ Q → P.Factors f → Q.Factors f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α},
  (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachStateRefT'OfLawfulMonad : ∀ {m : Type → Type} {ω σ : Type} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m],
  WeaklyLawfulMonadAttach (StateRefT' ω σ m)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonneg_iff_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → (0 ≤ Real.logb b x ↔ x ≤ 1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instAddCommGroup : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → AddCommGroup (SchwartzMap E F)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAlgebra : {σ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra R (MvPowerSeries σ A)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- a family of linear maps `M₁.obj X ⟶ M₂.obj X` for all `X`.  -/
PresheafOfModules.Hom.app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M₁ M₂ : PresheafOfModules R} → M₁.Hom M₂ → (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The name of the relation.  -/
Mathlib.Tactic.ClickSuggestions.GrwPos.relName : Mathlib.Tactic.ClickSuggestions.GrwPos → Lean.Name
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.Sum.dist_comm : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (x y : X ⊕ Y),
  Metric.Sum.dist x y = Metric.Sum.dist y x
-- Mathlib.Data.PFun
PFun.prodLift_fst_comp_snd_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ),
  (f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) = f.prodMap g
-- Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Meta.NormNum.asc_factorial_aux : ∀ (n l m a b : ℕ), n.ascFactorial l = a → (n + l).ascFactorial m = b → n.ascFactorial (l + m) = a * b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_add_nat_mul_two_pi : ∀ (x : ℂ) (n : ℕ), Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x
-- Mathlib.Topology.Specialization
Specialization.ofEquiv_specializes_ofEquiv : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a b : Specialization α},
  Specialization.ofEquiv a ⤳ Specialization.ofEquiv b ↔ b ≤ a
-- Mathlib.Algebra.Order.Group.PosPart
posPart_max : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a b : α), (a ⊔ b)⁺ = a⁺ ⊔ b⁺
-- Lean.Parser.Command
Lean.Parser.Command.theorem : Lean.Parser.Parser
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedTerminationBy : Inhabited Lean.Elab.TerminationBy
-- Aesop.RuleSet
Aesop.instEmptyCollectionLocalRuleSet : EmptyCollection Aesop.LocalRuleSet
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_nsmul : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] [inst_7 : IsOrderedAddMonoid E₂] (f : E₁ →ₚ[R] E₂) (n : ℕ),
  (n • f).toLinearMap = n • f.toLinearMap
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp F p (μ.trim hm))),
  ↑↑↑(MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f) =ᵐ[μ] ↑↑f
-- Mathlib.Topology.Continuous
/-- See note [comp_of_eq lemmas]  -/
ContinuousAt.comp_of_eq : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {x : X} {y : Y} {g : Y → Z},
  ContinuousAt g y → ContinuousAt f x → f x = y → ContinuousAt (g ∘ f) x
-- Lean.Parser.Attr
Lean.Parser.Attr.export.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexRingEquiv_refl : ∀ {n : Type u_3} (R : Type u_11) [inst : Fintype n] [inst_1 : Mul R] [inst_2 : AddCommMonoid R],
  Matrix.reindexRingEquiv R (Equiv.refl n) = RingEquiv.refl (Matrix n n R)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.TreeMap.maxKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} [inst_1 : Monad n]
  [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_10 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n (ULift.{w, 0} Bool)} {init : γ}
  {g : β → γ → o (ForInStep γ)},
  forIn (Std.Iter.filterM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.all.inj : ∀ {subgoals subgoals_1 : Array Lean.MVarId},
  Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals = Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals_1 →
    subgoals = subgoals_1
-- Mathlib.Data.List.Defs
/-- Asynchronous version of `List.map`.
 -/
List.mapAsyncChunked : {α : Type u_7} → {β : Type u_8} → (α → β) → List α → optParam ℕ 1024 → List β
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_ofList : ∀ {α : Type u_1} (l : List α), FreeAddMonoid.toList (FreeAddMonoid.ofList l) = l
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapGrp_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
      ((F.comp G).map CategoryTheory.MonObj.mul)
-- Mathlib.Topology.Connected.Basic
IsConnected.isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → IsPreconnected s
-- Mathlib.RingTheory.Perfection
/-- The `n`-th coefficient of an element of the perfection.  -/
Perfection.coeff : (R : Type u_1) →
  [inst : CommSemiring R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [inst_1 : CharP R p] → ℕ → Perfection R p →+* R
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral in L1 space  -/
MeasureTheory.L1.integral : {α : Type u_5} →
  {E : Type u_6} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} → [NormedSpace ℝ E] → [CompleteSpace E] → ↥(MeasureTheory.Lp E 1 μ) → E
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup is closed under division.  -/
Subgroup.div_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x / y ∈ H
-- Mathlib.Logic.ExistsUnique
/-- The difference with `existsUnique_eq` is that the equality is reversed.  -/
existsUnique_eq' : ∀ {α : Sort u_1} {a' : α}, ∃! a, a' = a
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.diag_subinterval_eq : ∀ {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.diag l) (SimplexCategory.subinterval j l hjl) =
    SimplexCategory.intervalEdge j l hjl
-- Init.GrindInstances.ToInt
Lean.Grind.instAddUInt64UintOfNatNat : Lean.Grind.ToInt.Add UInt64 (Lean.Grind.IntInterval.uint 64)
-- Init.Data.SInt.Basic
/-- Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on
overflow.

Examples:
 * `Nat.toInt8 53 = 53`
 * `Nat.toInt8 127 = 127`
 * `Nat.toInt8 128 = -128`
 * `Nat.toInt8 255 = -1`
 -/
Nat.toInt8 : ℕ → Int8
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist_triangle_inl_inr_inr : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Z] (Φ : Z → X)
  (Ψ : Z → Y) (ε : ℝ) (x : X) (y z : Y),
  Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + Metric.glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_eq_zero : ∀ {x : GaussianInt}, GaussianInt.toComplex x = 0 ↔ x = 0
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.leftHomologyData_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.leftHomologyData.π = 0
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂),
  CategoryTheory.Comma.mapLeft R l =
    {
      obj := fun X =>
        { left := X.left, right := X.right, hom := CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom },
      map := fun {X Y} f => { left := f.left, right := f.right, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_multiples_iff : ∀ {M : Type u_1} [inst : AddMonoid M] (x z : M), x ∈ AddSubmonoid.multiples z ↔ ∃ n, n • z = x
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If a normed space is (topologically) non-trivial, then the norm of the identity equals `1`.  -/
ContinuousLinearMap.norm_id : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [NontrivialTopology E], ‖ContinuousLinearMap.id 𝕜 E‖ = 1
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_rio : ∀ {b : ℕ}, (*...b).toList.length = b
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.zero_apply : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (x : E₁), 0 x = 0
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.prodComm_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E H)
  (J : ModelWithCorners 𝕜 F G) (M : Type u_9) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] (N : Type u_11)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞),
  (Diffeomorph.prodComm I J M N n).symm = Diffeomorph.prodComm J I N M n
-- Lean.Meta.Tactic.LibrarySearch
/-- the forward direction of an `iff`  -/
Lean.Meta.LibrarySearch.DeclMod.mp : Lean.Meta.LibrarySearch.DeclMod
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.subset_compl_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t : Set X}, Metric.AreSeparated s t → s ⊆ tᶜ
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a separable metric space `X`, `denseSeq X : ℕ → X` gives a countable
dense sequence. This measures the distance between `denseSeq X n` and `x`, truncated to the unit
interval `I` so that the distances remain bounded.

The function `(fun x n ↦ distDenseSeq n x) : X → ℕ → I` is a mapping from `X` to the Hilbert cube.
 -/
Metric.PiNatEmbed.distDenseSeq : (X : Type u_3) → [inst : MetricSpace X] → [TopologicalSpace.SeparableSpace X] → ℕ → X → ↑unitInterval
-- Mathlib.Analysis.Convex.StdSimplex
/-- The map `stdSimplex S X → stdSimplex S Y` that is induced by a map `f : X → Y`.  -/
stdSimplex.map : {S : Type u_1} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {X : Type u_2} →
        {Y : Type u_3} →
          [inst_2 : Fintype X] →
            [inst_3 : Fintype Y] → [IsOrderedRing S] → (X → Y) → ↑(stdSimplex S X) → ↑(stdSimplex S Y)
-- Mathlib.Data.ENat.Lattice
ENat.iInf_natCast_ne_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι
-- Aesop.Index.Basic
Aesop.IndexingMode.hyps.inj : ∀ {keys keys_1 : Array Lean.Meta.DiscrTree.Key},
  Aesop.IndexingMode.hyps keys = Aesop.IndexingMode.hyps keys_1 → keys = keys_1
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_symm_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α),
  (Equiv.optionSubtypeNe a).symm b = if h : b = a then none else some ⟨b, h⟩
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.two_pi_pos : 0 < 2 * Real.pi
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.TreeMap.Raw.unitOfList (hd :: tl) cmp = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Init.Data.Nat.Basic
Nat.sub_lt_right_of_lt_add : ∀ {n k m : ℕ}, n ≤ k → k < m + n → k - n < m
-- Mathlib.Data.Set.Image
Set.image_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = Set.range fun x => f ↑x
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- The canonical isomorphism of an internal direct sum with the ambient algebra  -/
DirectSum.IsInternal.coeAlgEquiv : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {ι : Type u_7} →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] →
                {M : ι → Submodule R A} →
                  [inst_5 : SetLike.GradedMonoid M] → DirectSum.IsInternal M → (DirectSum ι fun i => ↥(M i)) ≃ₐ[R] A
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l).get k h = m.get k ⋯
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Data.Real.Basic
Real.instAddRightCancelSemigroup : AddRightCancelSemigroup ℝ
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I : Ideal S} {r : S},
  (∀ {x : S}, x * r = 0 → x = 0) →
    r ∈ I → ∀ {p : Polynomial R}, p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ Ideal.comap f I
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.fromZetaAut.eq_1 : ∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] {L : Type u_2} {μ : L} [inst_2 : CommRing L]
  [inst_3 : IsDomain L] (hμ : IsPrimitiveRoot μ n) [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L]
  (h : Irreducible (Polynomial.cyclotomic n K)),
  IsCyclotomicExtension.fromZetaAut hμ h = (IsCyclotomicExtension.autEquivPow L h).symm (ZMod.unitOfCoprime ⋯.choose ⋯)
-- Mathlib.Data.Fintype.OfMap
/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
arbitrary `Fintype` instances, use `Finset.univ_eq_empty`.  -/
Fintype.univ_ofIsEmpty : ∀ {α : Type u_1} [inst : IsEmpty α], Finset.univ = ∅
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_add_of_toNat_lt : ∀ {a b c : UInt8}, b.toNat + c.toNat < 8 → a <<< (b + c) = a <<< b <<< c