mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.match_1.eq_1 : ∀ {α : Type} (motive : List α → Sort u_1) (h_1 : Unit → motive []) (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Topology.Constructions
/-- Let `s` be a discrete subset of a topological space. Then the preimage of `s` by
a continuous injective map is also discrete.  -/
DiscreteTopology.preimage_of_continuous_injective : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set Y)
  [DiscreteTopology ↑s] {f : X → Y}, Continuous f → Function.Injective f → DiscreteTopology ↑(f ⁻¹' s)
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.ArgsPacker.mk.injEq : ∀ (varNamess varNamess_1 : Array (Array Lean.Name)),
  ({ varNamess := varNamess } = { varNamess := varNamess_1 }) = (varNamess = varNamess_1)
-- Mathlib.Algebra.Lie.Basic
/-- The identity map is a Lie module morphism.  -/
LieModuleHom.instOne : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → One (M →ₗ⁅R,L⁆ M)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_zero : { cauchy := 0 } = 0
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Pass.toConfig : Mathlib.TacticAnalysis.Pass → Mathlib.TacticAnalysis.Config
-- Mathlib.Order.BoundedOrder.Basic
OrderBot.mk : {α : Type u} → [inst : LE α] → [toBot : Bot α] → (∀ (a : α), ⊥ ≤ a) → OrderBot α
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_union_inter` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be finite.  -/
finprod_mem_union_inter' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  (s ∩ Function.mulSupport f).Finite →
    (t ∩ Function.mulSupport f).Finite →
      (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
        (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Order.Filter.Basic
Filter.eq_sInf_of_mem_iff_exists_mem : ∀ {α : Type u} {S : Set (Filter α)} {l : Filter α}, (∀ {s : Set α}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) → l = sInf S
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqDeclValue.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.DeclValue pu → Lean.Compiler.LCNF.DeclValue pu → Bool
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.instInhabitedScopedEntries : {a : Type} → Inhabited (Lean.ScopedEnvExtension.ScopedEntries a)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingSubmonoid_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] {s : Set α} {m : M},
  m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  AddCommMonCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.GeometricallyConnected f]
  [AlgebraicGeometry.GeometricallyConnected g] [AlgebraicGeometry.UniversallyOpen f]
  [AlgebraicGeometry.UniversallyOpen g],
  AlgebraicGeometry.GeometricallyConnected (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.neg : ∀ {R : Type u_1} {x : R} [inst : Ring R], IsNilpotent x → IsNilpotent (-x)
-- Init.Data.Array.Lemmas
Array.lawfulBEq_iff : ∀ {α : Type u_1} [inst : BEq α], LawfulBEq (Array α) ↔ LawfulBEq α
-- Mathlib.Order.Atoms
covBy_iff_atom_Ici : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} (h : a ≤ b), a ⋖ b ↔ IsAtom ⟨b, h⟩
-- Mathlib.Data.List.Defs
List.Forall.eq_def : ∀ {α : Type u_1} (p : α → Prop) (x : List α),
  List.Forall p x =
    match x with
    | [] => True
    | [x] => p x
    | x :: l => p x ∧ List.Forall p l
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.coe_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasureTheory.MeasureSpace E] [inst_5 : BorelSpace E]
  [inst_6 : SecondCountableTopology E] [inst_7 : MeasureTheory.volume.HasTemperateGrowth] (f : SchwartzMap E F)
  (g : SchwartzMap E ℂ), ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) g = ∫ (x : E), g x • f x
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAdd : {α : Type u_1} → [Add α] → Add (Colex α)
-- Mathlib.Algebra.Colimit.Ring
Field.DirectLimit.inv.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  [inst_3 : (i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) (p : Ring.DirectLimit G f),
  Field.DirectLimit.inv G f p = if H : p = 0 then 0 else Classical.choose ⋯
-- Std.Data.ExtDTreeMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.ExtDTreeMap.erase : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Std.ExtDTreeMap α β cmp
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instVAddSubtypeMem : {M' : Type u_1} → {α : Type u_2} → {S' : Type u_4} → [inst : SetLike S' M'] → (s : S') → [VAdd M' α] → VAdd (↥s) α
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toSubalgebra_injective : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A], Function.Injective StarSubalgebra.toSubalgebra
-- Init.Data.Vector.Find
Vector.findSome?_replicate_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isNone = true → Vector.findSome? f (Vector.replicate n a) = none
-- Mathlib.Algebra.Group.Even
instDecidablePredAddOppositeEven.eq_1 : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidablePred Even] (x : αᵃᵒᵖ),
  instDecidablePredAddOppositeEven x = decidable_of_iff (Even (AddOpposite.unop x)) ⋯
-- Mathlib.Topology.Maps.Strict.Module
/-- A linear map is strict if and only if its `rangeRestrict` is an open quotient map.  -/
LinearMap.isStrictMap_iff_isOpenQuotientMap_rangeRestrict : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S}
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module S N] {f : M →ₛₗ[σ] N}
  [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace N] [IsTopologicalAddGroup M] [inst_9 : RingHomSurjective σ],
  Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousOn.upperSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} {s : Set α},
  UpperSemicontinuousOn f s → x ∈ s → UpperSemicontinuousWithinAt f s x
-- Mathlib.Data.Num.Basic
/-- Converts a `ZNum` to an `Option Num`, where `ofZNum' p = none` if `p < 0`.  -/
Num.ofZNum' : ZNum → Option Num
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_pow_right_iff : ∀ {n : ℕ}, 0 < n → ∀ (a b : ℕ), a.Coprime (b ^ n) ↔ a.Coprime b
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.root.inj : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} {h : x.dest = ⟨a, f⟩}
  {i : Fin2 n} {c : P.drop.B a i} {a_1 : P.A} {f_1 : P.last.B a_1 → P.last.M} {h_1 : x.dest = ⟨a_1, f_1⟩}
  {c_1 : P.drop.B a_1 i},
  MvPFunctor.M.Path.root x a f h i c = MvPFunctor.M.Path.root x a_1 f_1 h_1 i c_1 → a = a_1 ∧ f ≍ f_1 ∧ c ≍ c_1
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_top : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S], Ideal.absNorm ⊤ = 1
-- Init.Data.Array.Erase
Array.erase_filter : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {f : α → Bool} {xs : Array α},
  (Array.filter f xs).erase a = Array.filter f (xs.erase a)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
FiberwiseLinear.openPartialHomeomorph.eq_1 : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {U : Set B} (φ : B → F ≃L[𝕜] F) (hU : IsOpen U)
  (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U),
  FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ =
    { toFun := fun x => (x.1, (φ x.1) x.2), invFun := fun x => (x.1, (φ x.1).symm x.2), source := U ×ˢ Set.univ,
      target := U ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
      continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles._auto_3),
  CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) = 0
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsNonneg.add : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Preorder R] [AddLeftMono R] {B C : LinearMap.BilinForm R M}, B.IsNonneg → C.IsNonneg → (B + C).IsNonneg
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β},
  s ⊆ s' → Finset.image₂ f s t ⊆ Finset.image₂ f s' t
-- Mathlib.CategoryTheory.Retract
CategoryTheory.NatTrans.retractArrowApp_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) {X Y : C} (h : CategoryTheory.Retract X Y),
  (CategoryTheory.NatTrans.retractArrowApp τ h).i = CategoryTheory.Arrow.homMk (F.map h.i) (G.map h.i) ⋯
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal_pos_apply : ∀ {e : NNReal} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)}, x = 0 → (WithZeroMulInt.toNNReal he) x = 0
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G)
  (a : F.Grothendieck),
  ((CategoryTheory.Pseudofunctor.Grothendieck.map α).obj a).fiber = (α.app { as := a.base }).toFunctor.obj a.fiber
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  Std.DHashMap.Raw.Const.get (m₁ ∩ m₂) k h_mem = Std.DHashMap.Raw.Const.get m₁ k ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.MeasureSpace.mk : {α : Type u_6} → [toMeasurableSpace : MeasurableSpace α] → MeasureTheory.Measure α → MeasureTheory.MeasureSpace α
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8Size_le_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {c : Char}, b.utf8DecodeChar? 0 = some c → c.utf8Size ≤ b.size
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_aleph0_iff_set_countable : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s ≤ Cardinal.aleph0 ↔ s.Countable
-- Init.Prelude
Lean.instAppendName : Append Lean.Name
-- Qq.Match
Qq.Impl.PatternVar : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.abs_eq_zero : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → AddGroup (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftMono (α i)] [∀ (i : ι), AddRightMono (α i)], |f| = 0 ↔ f = 0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_min : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    ∀ {m : ℕ},
      m < MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i → ¬MeasureTheory.SignedMeasure.ExistsOneDivLT✝ s i m
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList.congr_simp : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Ric α), r = r_1 → r.toList = r_1.toList
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Ioo : ∀ (a b : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Ioo a b)
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.Products.nil.eq_1 : ∀ {I : Type u} [inst : LinearOrder I], Profinite.NobelingProof.Products.nil = ⟨[], ⋯⟩
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep_of_iIndep_of_le : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m₁ m₂ : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndep m₂ κ μ → (∀ (i : ι), m₁ i ≤ m₂ i) → ProbabilityTheory.Kernel.iIndep m₁ κ μ
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- A variant of `eq_inv_mul_iff_mul_eq₀` that moves the nonzero hypothesis to another variable.  -/
mul_eq_of_eq_inv_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → b = a⁻¹ * c → a * b = c
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α} {fallback : Unit},
  (Std.ExtTreeMap.unitOfList l cmp).getD k fallback = ()
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coeff_zero_eq_aeval_zero' : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Polynomial R),
  (algebraMap R A) (p.coeff 0) = (Polynomial.aeval 0) p
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.padicNormE_lim_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f : CauSeq ℚ_[p] norm} {a : ℝ}, 0 < a → (∀ (i : ℕ), ‖↑f i‖ ≤ a) → ‖f.lim‖ ≤ a
-- Lean.Meta.Tactic.Congr
/-- Try to apply a `simp` congruence theorem.
 -/
Lean.MVarId.congr? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.mk.congr_simp : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x),
  { toFun := toFun, map_formula' := map_formula' } = { toFun := toFun_1, map_formula' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearMap.toUniformConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {𝔖 : Set (Set E)} {A : E →SL[σ] F} {x : E},
  ((ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖) A) x = A x
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.equivalenceSingleObjInverse_obj_obj : ∀ (R : Type) [inst : Ring R] (X : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)),
  ((CategoryTheory.Mat.equivalenceSingleObjInverse R).obj X).obj = X.ι
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instIsFractionRingResidueFieldBotIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], IsFractionRing R ⊥.ResidueField
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.coe_add : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S'),
  ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Module.NatInt
/-- All `ℕ`-module structures are equal. See also `AddCommMonoid.uniqueNatModule`.  -/
AddCommMonoid.subsingletonNatModule : ∀ {M : Type u_3} [inst : AddCommMonoid M], Subsingleton (Module ℕ M)
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty.eq_4 : Lean.Grind.IntInterval.ii.nonEmpty = true
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint over `F`, then the
rank of `A ⊔ B` is equal to the product of that of `A` and `B`.  -/
IntermediateField.LinearDisjoint.rank_sup : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B → Module.rank F ↥(A ⊔ B) = Module.rank F ↥A * Module.rank F ↥B
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} (h' : a ∈ m), m[a]? = some m[a]
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.pure_eq_pure : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type w} {a : α}, pure a = Std.Iterators.PostconditionT.pure a
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.id_comp : ∀ {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₂] (f : E₁ →ₚ[R] E₂), (PositiveLinearMap.id R E₂).comp f = f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_le_sin_of_le_of_le_pi_div_two : ∀ {x y : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → x ≤ y → Real.sin x ≤ Real.sin y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.addPolynomial_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y ℓ : R),
  W'.addPolynomial x y ℓ =
    -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
          c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
          d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_pair : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, {a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_eraseMax : ∀ {α : Type u_1} (t : Ordnode α), t.eraseMax.dual = t.dual.eraseMin
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance2.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (c : RBTree.RBNode α) (z : α) (d_1 : RBTree.RBNode α), d = RBTree.RBNode.node RBTree.RBColor.red c z d_1 → False) →
    (match a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d with
      | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) =>
        h_1 a x b y c z d
      | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d =>
        h_2 a x b y c z d
      | a, x, b => h_3 a x b) =
      h_2 a x b y c z d
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.bddAbove_range_agmSequences_fst : ∀ {x y : NNReal}, BddAbove (Set.range fun n => (x.agmSequences y n).1)
-- Mathlib.Data.Array.Defs
/-- Permute the array using a sequence of indices defining a cyclic permutation.
If the list of indices `l = [i₁, i₂, ..., iₙ]` are all distinct then
`(cyclicPermute! a l)[iₖ₊₁] = a[iₖ]` and `(cyclicPermute! a l)[i₀] = a[iₙ]`  -/
Array.cyclicPermute! : {α : Type u} → [Inhabited α] → Array α → List ℕ → Array α
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The functor `Spec.toLocallyRingedSpace : CommRingCatᵒᵖ ⥤ LocallyRingedSpace`
is fully faithful.  -/
AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.FullyFaithful
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_ofNormedAddCommGroup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (f : α → β)
  (Hf : Continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C), ⇑(BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H) = f
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instIsCharPInt64HPowNatOfNat : Lean.Grind.IsCharP Int64 (2 ^ 64)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_extractLsb' : ∀ {n s m : ℕ} {x : BitVec n}, (BitVec.extractLsb' s m x).toInt = (↑(x.toNat >>> s)).bmod (2 ^ m)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
trailing coefficient of `f₁ + f₂` at `x` is the sum of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x →
        meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0 →
          meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
-- Mathlib.Data.Int.ModEq
Int.modEq_neg : ∀ {n a b : ℤ}, a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f : ℕ → M` has sum `m`, then the partial sums `∑ i ∈ range n, f i` converge
to `m`.  -/
HasSum.tendsto_sum_nat : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℕ → M},
  HasSum f m → Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds m)
-- Mathlib.Algebra.WithConv
WithConv.congrLinearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] (f : A ≃ₗ[R] B) (x : WithConv A),
  (WithConv.congrLinearEquiv f) x = WithConv.toConv (f x.ofConv)
-- Mathlib.Logic.UnivLE
UnivLE.small : ∀ [self : UnivLE.{u, v}] (α : Type u), Small.{v, u} α
-- Mathlib.Order.Lattice
le_of_inf_le_sup_le : ∀ {α : Type u} [inst : DistribLattice α] {x y z : α}, x ⊓ z ≤ y ⊓ z → x ⊔ z ≤ y ⊔ z → x ≤ y
-- Init.Conv
/-- `trace_state` prints the current goal state.  -/
Lean.Parser.Tactic.Conv.convTrace_state : Lean.ParserDescr