mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_mor₃ : ∀ {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₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  h.triangle.mor₃ = CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)
-- Mathlib.Order.Antisymmetrization
instSymmAntisymmRel : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (AntisymmRel r)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodComm_symm : ∀ (α : Type u_9) (β : Type u_10), (Equiv.prodComm α β).symm = Equiv.prodComm β α
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q)
  (φ φ_1 : ↥p →L[R] F),
  φ = φ_1 →
    ∀ (ψ ψ_1 : ↥q →L[R] F),
      ψ = ψ_1 → ContinuousLinearMap.ofIsTopCompl h φ ψ = ContinuousLinearMap.ofIsTopCompl h φ_1 ψ_1
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.isOpen_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f → ∀ {s : Set Y}, IsOpen (f ⁻¹' s) ↔ IsOpen s
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.PreservesProduct.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G],
  CategoryTheory.Limits.PreservesProduct.iso G f = CategoryTheory.Limits.PreservesProduct.iso G f
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedVarId : Inhabited Lean.IR.VarId
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n]
  [inst_2 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂)
  [inst_7 : Fintype m] {M₃ : Type u_7} [inst_8 : AddCommMonoid M₃] [inst_9 : Module R M₃] (v₃ : Module.Basis l R M₃)
  [inst_10 : Finite l] [inst_11 : DecidableEq m] (A : Matrix l m R) (B : Matrix m n R),
  (Matrix.toLin v₁ v₃) (A * B) = (Matrix.toLin v₂ v₃) A ∘ₗ (Matrix.toLin v₁ v₂) B
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.Coindep.delete_spanning_iff : ∀ {α : Type u_1} {M : Matroid α} {D S : Set α}, M.Coindep D → ((M.delete D).Spanning S ↔ M.Spanning S ∧ Disjoint S D)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natAbs_pos : ∀ {n : ℤ} {a : ℕ}, Mathlib.Meta.NormNum.IsNat n a → Mathlib.Meta.NormNum.IsNat n.natAbs a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] [T2Space β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ MeasureTheory.SigmaFinite (μ.restrict t)
-- Mathlib.Topology.Sober
/-- A space is sober if every irreducible closed subset has a generic point.  -/
QuasiSober : (α : Type u_3) → [TopologicalSpace α] → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_le_coeff : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_eq_coeff_cert lhs rhs p k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Poly.denote' ctx p ≤ 0)
-- Mathlib.Order.Hom.Basic
StrictMono.denselyOrdered_range : ∀ {X : Type u_6} {Y : Type u_7} [inst : LinearOrder X] [DenselyOrdered X] [inst_2 : Preorder Y] {f : X → Y},
  StrictMono f → DenselyOrdered ↑(Set.range f)
-- Std.Http.Data.Status
/-- The numeric status code.
 -/
Std.Http.CustomStatus.code : Std.Http.CustomStatus → UInt16
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.Const.getEntryLTD k r (ky, y)
    else Std.DTreeMap.Internal.Impl.Const.getEntryLT k l ⋯ ⋯
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_zero : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  iterateFrobeniusEquiv R p 0 = RingEquiv.refl R
-- Mathlib.MeasureTheory.PiSystem
/-- For a `π`-system `C` over `α` and a sequence of sets `s` belonging to `C`,
`dissipate s n` belongs to `C`.  -/
IsPiSystem.dissipate_mem : ∀ {α : Type u_1} {s : ℕ → Set α} {C : Set (Set α)},
  IsPiSystem C → (∀ (n : ℕ), s n ∈ C) → ∀ (n : ℕ), (Set.dissipate s n).Nonempty → Set.dissipate s n ∈ C
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.innerProp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [InnerProductSpaceable E] (r : 𝕜), InnerProductSpaceable.innerProp'✝ E r
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left.  -/
vectorSpan_eq_span_vsub_set_left : ∀ (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 => p -ᵥ x) '' s)
-- Std.Http.Protocol.H1.Reader
/-- The current state of the machine.
 -/
Std.Http.Protocol.H1.Reader.state : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_op_of_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasLimit F.op
-- Mathlib.Data.PFun
/-- Graph of a partial function `f` as the set of pairs `(x, f x)` where `x` is in the domain of
`f`.  -/
PFun.graph : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set (α × β)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [NoZeroDivisors α], NoZeroDivisors (Lex α)
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.instCoeSort : {L : FirstOrder.Language} → (T : L.Theory) → CoeSort T.ModelType (Type w)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_iff_finMeasSupp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : MeasureTheory.SimpleFunc α E}, p ≠ 0 → p ≠ ⊤ → (MeasureTheory.MemLp (⇑f) p μ ↔ f.FinMeasSupp μ)
-- Batteries.Data.Fin.Coding
Fin.decodeFun.eq_def : ∀ {n : ℕ} (x : ℕ) (x_1 : Fin (n ^ x)),
  Fin.decodeFun x_1 =
    match (motive := (x : ℕ) → Fin (n ^ x) → Fin x → Fin n) x, x_1 with
    | 0, x => fun x => nomatch x
    | m.succ, ⟨k, hk⟩ =>
      have hn := ⋯;
      fun x =>
      match x with
      | ⟨0, ⋯⟩ => ⟨k % n, ⋯⟩
      | ⟨i.succ, hi⟩ =>
        have h := ⋯;
        Fin.decodeFun ⟨k / n, h⟩ ⟨i, ⋯⟩
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.maxD fallback = fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_lt_abs_eval_T_real : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < |x| → 1 < |Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)|
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `(F ⋙ forget AddCommGrpCat).sections` is `u`-small, `F` has a limit.  -/
AddCommGrpCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.span.eq_1 : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (S : Set A),
  DividedPowers.SubDPIdeal.span hI S = sInf {J | S ⊆ ↑J.carrier}
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightHom_toLinearMap : ∀ {ι : 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] {P : RootPairing ι R M N} (g : P.Aut),
  ↑(MulOpposite.unop ((RootPairing.Equiv.coweightHom P) g)) = MulOpposite.unop ((RootPairing.Hom.coweightHom P) ↑g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toArray_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.keys.toArray = t.keysArray
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.closure.eq_1 : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R), Subsemiring.closure s = sInf {S | s ⊆ ↑S}
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X)
  (x : ↑(F.obj.obj (Opposite.op (U ⊔ V)))),
  (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).1 =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index.eq_1 : ∀ {G : Type u_1} [inst : Group G] (K V : Set G),
  MeasureTheory.Measure.haar.index K V = sInf (Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V})
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.union m₂).getKey? k = m₂.getKey? k
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.mem_kaplanskySet_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Subsemigroup R} {P : Ideal R},
  P ∈ UniqueFactorizationMonoid.kaplanskySet✝ S ↔ ↑P ∩ ↑S = ∅
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap_replicate.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.merge.eq_4 : ∀ {α : Type u_1} (le : α → α → Bool) (a₁ : α) (c₁ sibling : Batteries.PairingHeapImp.Heap α) (a₂ : α)
  (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
      (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1) =
    if le a₁ a₂ = true then
      Batteries.PairingHeapImp.Heap.node a₁ (Batteries.PairingHeapImp.Heap.node a₂ c₂ c₁)
        Batteries.PairingHeapImp.Heap.nil
    else
      Batteries.PairingHeapImp.Heap.node a₂ (Batteries.PairingHeapImp.Heap.node a₁ c₁ c₂)
        Batteries.PairingHeapImp.Heap.nil
-- Init.Data.Nat.Basic
Nat.sub_succ : ∀ (n m : ℕ), n - m.succ = (n - m).pred
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Ideal R}
  [inst_3 : P.IsPrime] [Algebra.IsIntegral R S],
  Algebra.IsIntegral (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt_def_of_notMem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → Bundle.Trivialization.linearMapAt R e b = 0
-- Lean.Data.Lsp.Internal
/-- Unnamed identifier. These are used for all local references.  -/
Lean.Lsp.RefIdent.fvar : String → String → Lean.Lsp.RefIdent
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.step_iter : ∀ {β : Type w} {array : Array β},
  array.iter.step =
    if h : 0 < array.size then Std.PlausibleIterStep.yield (array.iterFromIdx 1) array[0] ⋯
    else Std.PlausibleIterStep.done ⋯
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_adjoin_simple_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
  Module.rank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.LocallyOfFinitePresentation f],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.Order.Antisymmetrization
/-- Turns an order homomorphism from `α` to `β` into one from `Antisymmetrization α` to
`Antisymmetrization β`. `Antisymmetrization` is actually a functor. See `Preorder_to_PartialOrder`.
 -/
OrderHom.antisymmetrization : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (α →o β) → (Antisymmetrization α fun x1 x2 => x1 ≤ x2) →o Antisymmetrization β fun x1 x2 => x1 ≤ x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) → [grp : CategoryTheory.GrpObj X] → [comm : CategoryTheory.IsCommMonObj X] → CategoryTheory.CommGrp C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.epi_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPushout → ∀ [CategoryTheory.Epi sq.f₁₂], CategoryTheory.Epi sq.f₃₄
-- Init.Data.Rat.Basic
/-- The denominator of the rational number is a natural number.  -/
Rat.den : ℚ → ℕ
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addEntryFn : {α β σ : Type} →
  Lean.ScopedEnvExtension.Descr α β σ →
    Lean.ScopedEnvExtension.StateStack α β σ →
      Lean.ScopedEnvExtension.Entry β → Lean.ScopedEnvExtension.StateStack α β σ
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.one_div_add_one_div : ∀ {p q r : NNReal}, p.HolderTriple q r → 1 / p + 1 / q = 1 / r
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofIntTruncate : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofIntClamp n).toBitVec = BitVec.ofInt 8 n
-- Std.Http.Data.URI.Basic
Std.Http.URI.instDecidableEqPort : DecidableEq Std.Http.URI.Port
-- Aesop.RuleSet
Aesop.BaseRuleSet.mk : Aesop.Index Aesop.NormRuleInfo →
  Aesop.Index Aesop.UnsafeRuleInfo →
    Aesop.Index Aesop.SafeRuleInfo →
      Lean.PHashMap Lean.Name (Option Lean.Name) →
        Aesop.ForwardIndex →
          Lean.PHashSet Aesop.RuleName →
            Aesop.RulePatternIndex →
              Lean.PHashSet Aesop.RuleName →
                Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName) → Aesop.BaseRuleSet
-- Mathlib.Analysis.Calculus.Deriv.Support
HasDerivAt.of_notMem_tsupport : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, x ∉ tsupport f → HasDerivAt f 0 x
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_iff_eq_one : ∀ {G : Type u_1} [inst : Monoid G] [IsMulTorsionFree G] (a : G), IsOfFinOrder a ↔ a = 1
-- Mathlib.Tactic.CongrExclamation
/-- For type arguments that are implicit or have forward dependencies, whether or not `congr!`
should generate equalities even if the types do not look plausibly equal.

We have a heuristic in the main congruence generator that types
`α` and `β` are *plausibly equal* according to the following algorithm:

- If the types are both propositions, they are plausibly equal (`Iff`s are plausible).
- If the types are from different universes, they are not plausibly equal.
- Suppose in whnf we have `α = f a₁ ... aₘ` and `β = g b₁ ... bₘ`. If `f` is not definitionally
  equal to `g` or `m ≠ n`, then `α` and `β` are not plausibly equal.
- If there is some `i` such that `aᵢ` and `bᵢ` are not plausibly equal, then `α` and `β` are
  not plausibly equal.
- Otherwise, `α` and `β` are plausibly equal.

The purpose of this is to prevent considering equalities like `ℕ = ℤ` while allowing equalities
such as `Fin n = Fin m` or `Subtype p = Subtype q` (so long as these are subtypes of the
same type).

The way this is implemented is that when the congruence generator is comparing arguments when
looking at an equality of function applications, it marks a function parameter as "fixed" if the
provided arguments are types that are not plausibly equal. The effect of this is that congruence
succeeds only if those arguments are defeq at `transparency` transparency.  -/
Congr!.Config.typeEqs : Congr!.Config → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} {x y : R},
  WeierstrassCurve.Δ W ≠ 0 → (W.Equation x y ↔ W.Nonsingular x y)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZero P]
  (hnp : N →+ P) (hmn : M →+ N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.FieldTheory.Separable
/-- An element `x` of an algebra `K` over a commutative ring `F` is said to be *separable*, if its
minimal polynomial over `K` is separable. Note that the minimal polynomial of any element not
integral over `F` is defined to be `0`, which is not a separable polynomial.
 -/
IsSeparable : (F : Type u_1) → {K : Type u_3} → [inst : CommRing F] → [inst_1 : Ring K] → [Algebra F K] → K → Prop
-- Mathlib.Algebra.Lie.Ideal
/-- An ideal of a Lie algebra is a Lie subalgebra.  -/
LieIdeal.toLieSubalgebra : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L → LieSubalgebra R L
-- Std.Sat.CNF.Basic
Std.Sat.CNF.mk : {α : Type u} → Array (Std.Sat.CNF.Clause α) → Std.Sat.CNF α
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableProducts.out : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableProducts C]
  (J : Type) [Countable J], CategoryTheory.Limits.HasProductsOfShape J C
-- Init.Data.Fin.OverflowAware
Fin.addNat?_zero : ∀ {n : ℕ} {i : Fin n}, i.addNat? 0 = some i
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.snd_ne_fst : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.toProd.2 ≠ d.toProd.1
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.flatMapM.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Init.Data.String.Basic
/-- Efficiently checks whether a position is at a UTF-8 character boundary of the slice `s`.  -/
String.Pos.Raw.isValidForSlice : String.Slice → String.Pos.Raw → Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_inter_add_sum_sdiff : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → M),
  ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, f x = ∑ x ∈ s, f x
-- Std.Time.Format.Basic
/-- The format string used for parsing and formatting.
 -/
Std.Time.GenericFormat.string : {awareness : Std.Time.Awareness} → Std.Time.GenericFormat awareness → Std.Time.FormatString
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_list_sum_left : ∀ {α : Type u_6} {a : Multiset α} {l : List (Multiset α)}, Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (t.insertManyIfNewUnit l).getKey! k = t.getKey! k
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_sum : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommMonoid Y] {ι : Type u_3}
  {s : Finset ι} {F : ι → Function.locallyFinsuppWithin U Y}, ⇑(∑ n ∈ s, F n) = ∑ n ∈ s, ⇑(F n)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w<b`.
See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices.  -/
DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {b : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b