mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instSupSet : {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] → SupSet (LieSubmodule R L M)
-- Lean.MetavarContext
Lean.instInhabitedMetavarKind : Inhabited Lean.MetavarKind
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β))
  (target : { d // 0 < d.size }),
  Std.DHashMap.Internal.Raw₀.expand.go✝ i source target =
    if h : i < source.size then
      have es := source[i];
      have source := source.set i Std.DHashMap.Internal.AssocList.nil h;
      have target := Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target es;
      Std.DHashMap.Internal.Raw₀.expand.go✝ (i + 1) source target
    else target
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.RawView.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (k : α) (v : β k)
  (tree : Std.DTreeMap.Internal.Impl α β),
  sizeOf { k := k, v := v, tree := tree } = 1 + sizeOf k + sizeOf v + sizeOf tree
-- Init.Prelude
/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇`  -/
Lean.Name.mkStr7 : String → String → String → String → String → String → String → Lean.Name
-- Mathlib.NumberTheory.LucasLehmer
mersenne_odd : ∀ {p : ℕ}, Odd (mersenne p) ↔ p ≠ 0
-- Mathlib.GroupTheory.FreeGroup.Orbit
/-- Applying `w⁻¹` to the orbit generated by all elements of a free group that start with `w` yields
the orbit generated by all the words that start with every letter except `w⁻¹`
(and the original point).
 -/
FreeGroup.Orbit.duplicate : ∀ {α : Type u_1} {X : Type u_2} [inst : DecidableEq α] [inst_1 : MulAction (FreeGroup α) X] (x : X) (w : α × Bool),
  {x_1 | ∃ y ∈ MulAction.orbit (↑(FreeGroup.startsWith w)) x, (FreeGroup.mk [w])⁻¹ • y = x_1} =
    (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(FreeGroup.startsWith v)) x) ∪ {x}
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A category with finite biproducts has a zero object.  -/
CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C], CategoryTheory.Limits.HasZeroObject C
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instInhabitedOffset : Inhabited Std.Time.Hour.Offset
-- Init.Data.Nat.Lemmas
Nat.div_dvd_div : ∀ {m n k : ℕ}, k ∣ m → m ∣ n → m / k ∣ n / k
-- Mathlib.Topology.Algebra.FilterBasis
/-- If an additive group is endowed with a topological structure coming from an
additive group filter basis, then it's an additive topological group.  -/
AddGroupFilterBasis.isTopologicalAddGroup : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), IsTopologicalAddGroup G
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- Conjugates of `SL(2, ℤ)` by `GL(2, ℚ)` are arithmetic subgroups.  -/
CongruenceSubgroup.isArithmetic_conj_SL2Z : ∀ (g : GL (Fin 2) ℚ),
  (ConjAct.toConjAct ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g) •
      (Matrix.SpecialLinearGroup.mapGL ℝ).range).IsArithmetic
-- Mathlib.Analysis.Convex.Topology
Convex.combo_interior_self_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ interior s → y ∈ s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ interior s
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_length_of_finiteDimensionalOrder : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : FiniteDimensionalOrder α],
  Order.krullDim α = ↑(LTSeries.longestOf α).length
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.unattach_toList_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α Id],
  (it.attachWith P hP).toList.unattach = it.toList
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_norm : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F}, MeasureTheory.eLpNorm' (fun a => ‖f a‖) q μ = MeasureTheory.eLpNorm' f q μ
-- Mathlib.Topology.GDelta.Basic
/-- An intersection with a meagre set is meagre.  -/
IsMeagre.inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsMeagre s → IsMeagre (s ∩ t)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_coe : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂), ↑(Submodule.comap f p) = ⇑f ⁻¹' ↑p
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioi : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ioi ↑x = Set.Ioi x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.comp_symm_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : N → α) (g : M → α), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq.injEq : ∀ (a b : Lean.Expr) (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (la_1 lb_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a b la lb =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a_1 b_1 la_1 lb_1) =
    (a = a_1 ∧ b = b_1 ∧ la = la_1 ∧ lb = lb_1)
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- (Implementation): Underlying functor of associated relative gluing datum.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                      CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Star.Free
/-- The star ring formed by reversing the elements of products  -/
FreeAlgebra.instStarRing : {R : Type u_1} → [inst : CommSemiring R] → {X : Type u_2} → StarRing (FreeAlgebra R X)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.involutiveNeg : {α : Type u} → [InvolutiveInv α] → InvolutiveNeg (Additive α)
-- Mathlib.Tactic.ProdAssoc
/-- Converts a term `e` in an iterated product `P1` into a term of an iterated product `P2`.
Here `e` is an `Expr` representing the term, and the iterated products are represented
by terms of `ProdTree`.  -/
Lean.Expr.ProdTree.convertTo : Lean.Expr.ProdTree → Lean.Expr.ProdTree → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_restr : ∀ {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] [inst_5 : LieAlgebra R L] {N : LieSubmodule R L M}
  {H : LieSubalgebra R L} {m : M}, m ∈ N.restr H ↔ m ∈ N
-- Lean.Data.Json.Parser
Lean.Json.Parser.objectCore : Std.TreeMap.Raw String Lean.Json compare → Std.Internal.Parsec.String.Parser (Std.TreeMap.Raw String Lean.Json compare)
-- Mathlib.Algebra.Lie.Prod
/-- The prod of two Lie algebra homomorphisms is a Lie algebra homomorphism.  -/
LieHom.prod : {R : Type u_1} →
  {L₁ : Type u_2} →
    {L₂ : Type u_3} →
      {L : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : LieRing L₁] →
            [inst_2 : LieAlgebra R L₁] →
              [inst_3 : LieRing L₂] →
                [inst_4 : LieAlgebra R L₂] →
                  [inst_5 : LieRing L] → [inst_6 : LieAlgebra R L] → (L →ₗ⁅R⁆ L₁) → (L →ₗ⁅R⁆ L₂) → L →ₗ⁅R⁆ L₁ × L₂
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜},
  HasGradientWithinAt f f' s x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → HasGradientWithinAt f₁ f' s x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.fun_inv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X Y : D) (f : X ⟶ Y),
  F.map (F.inv.map f) =
    CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X)
      (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulC_go : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ acc) =
    Lean.Grind.CommRing.Poly.denote ctx acc +
      Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Aesop.Options.Public
/-- Options which modify the behaviour of the `aesop` tactic.
 -/
Aesop.Options : Type
-- Mathlib.Order.Circular
OrderDual.instCircularOrder : (α : Type u_1) → [CircularOrder α] → CircularOrder αᵒᵈ
-- Batteries.Data.Fin.Coding
Fin.encodeSigma.eq_2 : ∀ (n_2 : ℕ) (f_2 : Fin (n_2 + 1) → ℕ) (i : ℕ) (hi : i + 1 < n_2 + 1) (j : Fin (f_2 ⟨i + 1, hi⟩)),
  Fin.encodeSigma f_2 ⟨⟨i.succ, hi⟩, j⟩ =
    match Fin.encodeSigma (fun x => f_2 x.succ) ⟨⟨i, ⋯⟩, j⟩ with
    | ⟨k, hk⟩ => ⟨f_2 0 + k, ⋯⟩
-- Mathlib.Data.Set.Prod
Set.prod_image_image_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {m₁ : α → γ} {m₂ : β → δ},
  (m₁ '' s) ×ˢ (m₂ '' t) = (fun p => (m₁ p.1, m₂ p.2)) '' s ×ˢ t
-- Mathlib.Data.ENNReal.Operations
ENNReal.iInf_add_iInf_of_monotone : ∀ {ι : Type u_2} [inst : Preorder ι] [IsCodirectedOrder ι] {f g : ι → ENNReal},
  Monotone f → Monotone g → iInf f + iInf g = ⨅ a, f a + g a
-- Init.Data.UInt.Bitwise
instAssociativeUInt32HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- A tagged prepartition is a partition if it covers the whole box.  -/
BoxIntegral.TaggedPrepartition.IsPartition : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → Prop
-- Mathlib.Data.Multiset.DershowitzManna
/-- If all elements of a multiset `M` are accessible with `<`, then the multiset `M` is
accessible given the `OneStep` relation.  -/
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.acc_oneStep_of_acc_lt : ∀ {α : Type u_1} [inst : Preorder α] {M : Multiset α}, (∀ x ∈ M, Acc LT.lt x) → Acc Multiset.OneStep✝ M
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Condition for `B` to be a filter basis on `A`.  -/
RingSubgroupsBasis.inter : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
  RingSubgroupsBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.range_basisSingleton : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
  [inst_3 : Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0),
  Set.range ⇑(FiniteDimensional.basisSingleton ι h v hv) = {v}
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulActionWithZero.mk : {M₀ : Type u_2} →
  {A : Type u_7} →
    [inst : MonoidWithZero M₀] →
      [inst_1 : Zero A] →
        [toMulAction : MulAction M₀ A] → (∀ (r : M₀), r • 0 = 0) → (∀ (m : A), 0 • m = 0) → MulActionWithZero M₀ A
-- Mathlib.Data.Seq.Basic
Stream'.Seq.update_nil : ∀ {α : Type u} (f : α → α) (n : ℕ), Stream'.Seq.nil.update n f = Stream'.Seq.nil
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instAdd : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Add G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffAdd I' n G] → Add (ContMDiffMap I I' N G n)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert b (Finset.Ico a b) = Finset.Ico a (Order.succ b)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.zero : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α], Matrix.IsAdjMatrix 0
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActionEntry.mk.sizeOf_spec : ∀ (declName : Lean.Name) (tacticKinds : Array Lean.Name),
  sizeOf { declName := declName, tacticKinds := tacticKinds } = 1 + sizeOf declName + sizeOf tacticKinds
-- Init.Data.UInt.Lemmas
USize.ofNat_sub : ∀ {a b : ℕ}, b ≤ a → USize.ofNat (a - b) = USize.ofNat a - USize.ofNat b
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_finsuppProd : ∀ {M : Type u_1} [inst : Zero M] {ι : Type u_2} (f : ι →₀ M) (g : ι → M → NNReal),
  ↑(f.prod g) = f.prod fun i m => ↑(g i m)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_le_of_brange_subset : ∀ {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}}
  {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}}, o.brange f ⊆ o'.brange g → o.blsub f ≤ o'.blsub g
-- Mathlib.RingTheory.WittVector.Truncated
/-- A ring homomorphism that truncates a truncated Witt vector of length `m` to
a truncated Witt vector of length `n`, for `n ≤ m`.
 -/
TruncatedWittVector.truncate : {p n : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] → {m : ℕ} → n ≤ m → TruncatedWittVector p m R →+* TruncatedWittVector p n R
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
hasSum_const_div_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a₁ a₂ : α},
  a₂ ≠ 0 → (HasSum (fun i => a₂ / f i) (a₂ * a₁) L ↔ HasSum (1 / f) a₁ L)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isInducedSubgraph_iff : ∀ {α : Type u_1} {β : Type u_2} (H G : Graph α β),
  H.IsInducedSubgraph G ↔
    H.IsSubgraph G ∧ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
tsum_mul_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α} [T2Space α], ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
-- Mathlib.NumberTheory.GaussSum
/-- A formula for the product of two Gauss sums with the same additive character.  -/
gaussSum_mul : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ φ : MulChar R R')
  (ψ : AddChar R R'), gaussSum χ ψ * gaussSum φ ψ = ∑ t, ∑ x, χ x * φ (t - x) * ψ t
-- Mathlib.LinearAlgebra.Prod
/-- The right injection into a product is a linear map.  -/
LinearMap.inr : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → M₂ →ₗ[R] M × M₂
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit : ∀ {γ : Type u_2} {α : Type u_3} [inst : SMul γ α] (a : α) (m : γ), m • a ∈ MulAction.orbit γ a
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ext_iff : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G}, η₁ = η₂ ↔ η₁.toNatTrans = η₂.toNatTrans
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.neg_mem : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A) {x : A},
  x ∈ S → -x ∈ S
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.isOpen_A_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} {r s : ℝ},
  Continuous (Function.uncurry f) → ∀ (L : E →L[𝕜] F), IsOpen {p | p.2 ∈ FDerivMeasurableAux.A (f p.1) L r s}
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ AddGrpCat AddMonCat)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.ext' : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {s : Submodule R E}
  {f g : ↥s →ₛₗ[σ] F}, f = g → { domain := s, toFun := f } = { domain := s, toFun := g }
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).contains k = true
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).length = min n p.length
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ClearInsertInductionMotive : {n : ℕ} →
  (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
    f.assignments.size = n →
      Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
        ℕ → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → Prop
-- Mathlib.Analysis.Analytic.Composition
AnalyticOnNhd.comp_analyticOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : F → G} {g : E → F} {s : Set F} {t : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOn 𝕜 g t → Set.MapsTo g t s → AnalyticOn 𝕜 (f ∘ g) t
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.oneGtZero.sizeOf_spec : sizeOf Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.oneGtZero = 1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_sup : ∀ {M : Type u_2} [inst : MulOneClass M] (S₁ S₂ : Submonoid M), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion.faithfulSMul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T), FaithfulSMul ↥S ↥T
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.hom_ext_iff : ∀ {R : Type u_1} [inst : NonAssocRing R] {d : ℤ} {f g : ℤ√d →+* R}, f = g ↔ f Zsqrtd.sqrtd = g Zsqrtd.sqrtd
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_functor_map_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) {X Y : CategoryTheory.Core C} (f : X ⟶ Y), (E.core.functor.map f).iso.inv = E.functor.map f.iso.inv
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.hasProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  (e : γ ≃ β), HasProd (f ∘ ⇑e) a ↔ HasProd f a
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Antitone fun x => Set.Ici (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  (sq : f₁ ⟶ f₁'),
  (sq₁₂.mapArrowLeft sq₁₂' sq).left =
    ⋯.desc (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Arrow.Hom.right sq)).app f₂.left) sq₁₂'.inl)
      (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Arrow.Hom.left sq)).app f₂.right) sq₁₂'.inr) ⋯
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_le_iff : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {C : ℝ},
  0 ≤ C →
    ∀ (i : ℕ) (f : ContDiffMapSupportedIn E F n K),
      (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.globalEquiv_naturality : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : WellFoundedLT ι] [inst_2 : SuccOrder ι] [inst_3 : InverseSystem f]
  (equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x })
  (equivLim : (i : ι) → Order.IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Set.Iio i)), ↑(e x) l = f ⋯ x }) ⦃i j : ι⦄
  (h : i ≤ j) (x : F j),
  (InverseSystem.globalEquiv equivSucc equivLim i) (f h x) =
    InverseSystem.piLTProj h ((InverseSystem.globalEquiv equivSucc equivLim j) x)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.between_le : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, SimpleGraph.between s t G ≤ G