mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Holor
Holor.CPRankMax.succ : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α] (n : ℕ) {ds : List ℕ} (x y : Holor α ds),
  x.CPRankMax1 → Holor.CPRankMax n y → Holor.CPRankMax (n + 1) (x + y)
-- Mathlib.Tactic.Hint
/-- An environment extension for registering hint tactics with priorities.  -/
Mathlib.Tactic.Hint.hintExtension : Lean.SimplePersistentEnvExtension (ℕ × Lean.TSyntax `tactic) (List (ℕ × Lean.TSyntax `tactic))
-- Init.Data.SInt.Lemmas
ISize.toInt_neg : ∀ (n : ISize), (-n).toInt = (-n.toInt).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Algebra.Divisibility.Units
/-- In a monoid, an element a divides an element b iff all associates of `a` divide `b`.  -/
IsUnit.mul_right_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b u : α}, IsUnit u → (a * u ∣ b ↔ a ∣ b)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getKeyLT?.go : {α : Type u} → {β : α → Type v} → [Ord α] → α → Option α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_X_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] (a : R), (Polynomial.X - Polynomial.C a).degree = 1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets
`U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is $C^n$ smooth on
`U i`, then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold.  -/
SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
  {f : SmoothPartitionOfUnity ι I M s} {n : ℕ∞} {U : ι → Set M} {g : ι → M → F},
  f.IsSubordinate U →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) (g i) (U i)) →
        ContMDiff I (modelWithCornersSelf ℝ F) ↑n fun x => ∑ᶠ (i : ι), (f i) x • g i x
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.prodRight_tmul_fst : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (B : Type u_6)
  (C : Type u_7) [inst_7 : Semiring B] [inst_8 : Semiring C] [inst_9 : Algebra R B] [inst_10 : Algebra R C] (a : A)
  (x : B × C), ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).1 = a ⊗ₜ[R] x.1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.fvarId : Lean.Elab.Term.LetRecToLift → Lean.FVarId
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  (F G : CategoryTheory.Functor (↑(Set.Iic x)) C) {k₁ k₂ : K} {h₁₂ : k₁ ≤ k₂} {h₂ : k₂ ≤ x},
  CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k₁ k₂ h₁₂ h₂ → F.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.mulExpNegSq_apply : ∀ (ε x : ℝ), ε.mulExpNegMulSq x = x * Real.exp (-(ε * x * x))
-- Mathlib.Algebra.Group.Units.Hom
Units.liftRight.eq_1 : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (g : M → Nˣ)
  (h : ∀ (x : M), ↑(g x) = f x), Units.liftRight f g h = { toFun := g, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.isLocalizationMap_iff_bijective : ∀ {M : Type u_1} {G : Type u_2} {F : Type u_3} [inst : CommMonoid M] [inst_1 : CommGroup G] {S : Submonoid G}
  [inst_2 : FunLike F G M] [MulHomClass F G M] {f : F}, S.IsLocalizationMap ⇑f ↔ Function.Bijective ⇑f
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiff_piLp_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  (p : ENNReal) [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞} {i : ι}, ContDiff 𝕜 n fun f => f.ofLp i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α},
  (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.replayConsts.replayKernel : Bool →
  Lean.Kernel.Environment →
    Lean.Kernel.Environment →
      Array (Lean.EnvExtension Lean.EnvExtensionState) →
        List Lean.AsyncConst✝ → Lean.Kernel.Environment → Except Lean.Kernel.Exception Lean.Kernel.Environment
-- Mathlib.Order.Antichain
isAntichain_and_least_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α], IsAntichain (fun x1 x2 => x1 ≤ x2) s ∧ IsLeast s a ↔ s = {a}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insert_le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t ≠ ∅}, (cmp ((t.insert k v).minKey ⋯) (t.minKey he)).isLE = true
-- Std.Http.Protocol.H1.Parser
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.hex.go : ℕ → ℕ → Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.Data.Rel
SetRel.preimage_subset_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → R.preimage t₁ ⊆ R.preimage t₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.push'.eq_1 : ∀ (k : Turing.PartrecToTM2.K'), Turing.PartrecToTM2.push' k = Turing.TM2.Stmt.push k fun x => x.getD default
-- Mathlib.Dynamics.BirkhoffSum.Average
map_birkhoffAverage : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (S : Type u_4) {F : Type u_5} {N : Type u_6} [inst_3 : DivisionSemiring S]
  [inst_4 : AddCommMonoid N] [inst_5 : Module S N] [inst_6 : FunLike F M N] [AddMonoidHomClass F M N] (g' : F)
  (f : α → α) (g : α → M) (n : ℕ) (x : α), g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring is closed under multiplication.  -/
Subring.mul_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
-- Mathlib.Logic.Relation
Relation.map_onFun_eq_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} {f : α → β},
  Function.Surjective f → Relation.Map (Function.onFun r f) f f = r
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_monomial : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ) (r : R),
  (p * (Polynomial.monomial n) r).coeff (d + n) = p.coeff d * r
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.composableArrows₃.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  HomologicalComplex.HomologySequence.composableArrows₃ K i j =
    CategoryTheory.ComposableArrows.mk₃ (K.homologyι i) (K.opcyclesToCycles i j) (K.homologyπ j)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α} {h' : a ∈ m}, m.getKey a h' = m.getKeyD a fallback
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.ext_iff : ∀ {G : Type u_1} [inst : AddGroup G] {t t' : TopologicalSpace G},
  IsTopologicalAddGroup G → IsTopologicalAddGroup G → (t = t' ↔ nhds 0 = nhds 0)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t : Cocone F.op` is a colimit cocone, then `t.unop : Cone F` is a limit cone.
 -/
CategoryTheory.Limits.IsColimit.unop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F.op} →
            CategoryTheory.Limits.IsColimit t → CategoryTheory.Limits.IsLimit t.unop
-- Mathlib.Order.Heyting.Basic
Disjoint.disjoint_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, Disjoint a b → Disjoint (a \ c) b
-- Mathlib.LinearAlgebra.Dual.Basis
/-- For any `m : M n`, $\sum_{p ∈ Q n} (ε p m) • e p = m$  -/
Module.DualBases.lc_coeffs : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (m : M), Module.DualBases.lc e (h.coeffs m) = m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.ExtDTreeMap.ofList l cmp}, (Std.ExtDTreeMap.ofList l cmp).get k' h = cast ⋯ v
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_setOfPred_re_le : ∀ (a : ℝ), interior {z | z.re ≤ a} = {z | z.re < a}
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver_cases_type.eq_1 : ∀ (p : ℕ → Prop), Int.Internal.Linear.OrOver_cases_type 0 p = p 0
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.mkGrindOnlyTactics.mkTac : Lean.TSyntax `Lean.Parser.Tactic.optConfig → Array Lean.Meta.Grind.TParam → Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.RingTheory.Localization.NormTrace
Algebra.traceMatrix_localizationLocalization : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] (M : Submonoid R) [inst_5 : IsLocalization M Rₘ] (Sₘ : Type u_5)
  [inst_6 : CommRing Sₘ] [inst_7 : Algebra S Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [inst_10 : IsScalarTower R Rₘ Sₘ] [inst_11 : IsScalarTower R S Sₘ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [inst_13 : Fintype ι]
  [inst_14 : DecidableEq ι] (b : Module.Basis ι R S),
  Algebra.traceMatrix Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) =
    (algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R ⇑b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharTwoJNeZeroNF] [CharP F 2],
  W.j ≠ 0
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfInstance : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Elab.DefView
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.mk.inj : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {inst : NontriviallyNormedField 𝕜} {inst_1 : NontriviallyNormedField 𝕜'} {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {F : Type u_4}
  {inst_4 : NormedAddCommGroup F} {inst_5 : NormedSpace 𝕜' F} {f : E →SL[σ] F} {toFun : F → E} {nnnorm : NNReal}
  {bound' : ∀ (y : F), ‖toFun y‖ ≤ ↑nnnorm * ‖y‖} {right_inv' : ∀ (y : F), f (toFun y) = y} {toFun_1 : F → E}
  {nnnorm_1 : NNReal} {bound'_1 : ∀ (y : F), ‖toFun_1 y‖ ≤ ↑nnnorm_1 * ‖y‖}
  {right_inv'_1 : ∀ (y : F), f (toFun_1 y) = y},
  { toFun := toFun, nnnorm := nnnorm, bound' := bound', right_inv' := right_inv' } =
      { toFun := toFun_1, nnnorm := nnnorm_1, bound' := bound'_1, right_inv' := right_inv'_1 } →
    toFun = toFun_1 ∧ nnnorm = nnnorm_1
-- Lean.Meta.Tactic.SolveByElim
/-- Applies the first possible lemma to the goal.  -/
Lean.Meta.SolveByElim.applyFirstLemma : Lean.Meta.SolveByElim.SolveByElimConfig →
  List (Lean.Elab.TermElabM Lean.Expr) →
    (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)) →
      Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {F : Set X},
  JoinedIn F x y → ∀ {f : X → Y}, Continuous f → JoinedIn (f '' F) (f x) (f y)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMax.eq_1 : ∀ {α : Type u_1}, Ordnode.nil.eraseMax = Ordnode.nil
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid have a representation of the base value in the `Monoid`.  -/
Units.instRepr : {α : Type u} → [inst : Monoid α] → [Repr α] → Repr αˣ
-- Lean.Server.InfoUtils
/-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`.  -/
Lean.Elab.InfoTree.hoverableInfoAtM? : {m : Type → Type u_1} →
  [inst : Monad m] →
    Lean.Elab.InfoTree →
      String.Pos.Raw →
        optParam Bool false →
          (optParam
              (Lean.Elab.ContextInfo →
                Lean.Elab.Info →
                  Lean.PersistentArray Lean.Elab.InfoTree →
                    List (Lean.Elab.HoverableInfoPrio × Lean.Elab.InfoWithCtx) →
                      m (List (Lean.Elab.HoverableInfoPrio × Lean.Elab.InfoWithCtx)))
              fun x x_1 x_2 results => pure results) →
            m (Option Lean.Elab.InfoWithCtx)
-- Mathlib.Data.Set.UnionLift
Set.preimage_iUnionLift : ∀ {α : Type u_1} {ι : Sort u_3} {β : Type u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  {hT : T ⊆ Set.iUnion S} (t : Set β),
  Set.iUnionLift S f hf T hT ⁻¹' t = Set.inclusion hT ⁻¹' ⋃ i, Set.inclusion ⋯ '' f i ⁻¹' t
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_eq_two : ∀ {α : Type u_1} {v : FreeMonoid α}, v.length = 2 ↔ ∃ c d, v = FreeMonoid.of c * FreeMonoid.of d
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Simplify an expression using only the axioms of a category.  -/
Mathlib.Tactic.Reassoc.categorySimp : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_eq_add : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] {f : α → M} (a b : α),
  a ≠ b → (∀ (x : α), x ≠ a ∧ x ≠ b → f x = 0) → ∑ x, f x = f a + f b
-- Init.Conv
/-- `norm_cast` tactic in `conv` mode.  -/
Lean.Parser.Tactic.Conv.normCast : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(ProjectiveSpectrum.vanishingIdeal t) = closure t
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  (∏ x ∈ s, if a = x then b x else 1) = if a ∈ s then b a else 1
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_zsmul : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f : X ⟶ Y} {r : ℤ},
  F.map (r • f) = r • F.map f
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.maximalIdeal_inj : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w₁ w₂ : NumberField.FinitePlace K),
  w₁.maximalIdeal = w₂.maximalIdeal ↔ w₁ = w₂
-- Mathlib.Data.ENat.Lattice
ENat.iSup_add : ∀ {ι : Sort u_2} {a : ℕ∞} [Nonempty ι] (f : ι → ℕ∞), (⨆ i, f i) + a = ⨆ i, f i + a
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The operator `fun x ↦ ⟪y, T x⟫` considered as a continuous linear operator
from `T.adjointDomain` to `𝕜`.  -/
LinearPMap.adjointDomainMkCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → (T : E →ₗ.[𝕜] F) → ↥T.adjointDomain → StrongDual 𝕜 ↥T.domain
-- Mathlib.Order.Filter.Pointwise
Filter.sub_eq_bot_iff : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, f - g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.reindex : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α],
  A.IsAdjMatrix → ∀ (f : V ≃ W), ((Matrix.reindex f f) A).IsAdjMatrix
-- Init.Data.Array.DecidableEq
Array.isEqv_self_beq : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] (xs : Array α), (xs.isEqv xs fun x1 x2 => x1 == x2) = true
-- Mathlib.Data.List.OfFn
List.forall_iff_forall_tuple : ∀ {α : Type u} {P : List α → Prop}, (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j j' : ι₄),
  (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).d j j' =
    HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' +
        HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' +
      HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j'
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquivClass.toZeroHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : MulZeroClass α]
  [inst_2 : MulZeroClass β] [MulEquivClass F α β], ZeroHomClass F α β
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeLeftOp_app : ∀ {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.leftOp ⟶ G.leftOp) (X : C),
  (CategoryTheory.NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).op
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_nat_eq_of_le_nat : ∀ {c : Cardinal.{u_1}} {n : ℕ}, c ≤ ↑n → ∃ m ≤ n, c = ↑m
-- Mathlib.Algebra.Homology.HomologySequence
/-- The diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j`.  -/
HomologicalComplex.HomologySequence.composableArrows₃ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Preadditive C] →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → [K.HasHomology i] → [K.HasHomology j] → CategoryTheory.ComposableArrows C 3
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Edge.mk.inj : ∀ {src dst : ℕ} {proof : Lean.Expr} {src_1 dst_1 : ℕ} {proof_1 : Lean.Expr},
  { src := src, dst := dst, proof := proof } = { src := src_1, dst := dst_1, proof := proof_1 } →
    src = src_1 ∧ dst = dst_1 ∧ proof = proof_1
-- Mathlib.MeasureTheory.Group.Prod
/-- The multiplicative shear mapping `(x, y) ↦ (x, xy)` preserves the measure `μ × ν`.
This condition is part of the definition of a measurable group in [Halmos, §59].
There, the map in this lemma is called `S`.  -/
MeasureTheory.measurePreserving_prod_mul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsMulLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Algebra.Regular.Basic
/-- An element is add-right-regular if and only if adding it on the right to
an add-right-regular element is add-right-regular.  -/
add_isAddRightRegular_iff : ∀ {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R),
  IsAddRightRegular a → (IsAddRightRegular (b + a) ↔ IsAddRightRegular b)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.alls.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.alls =
    match x, x_1 with
    | 0, φ => φ
    | _n.succ, φ => φ.all.alls
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.of.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B},
  HNNExtension.of = (HNNExtension.con G A B φ).mk'.comp Monoid.Coprod.inl
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ∃ a, t.contains a = true
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_assoc_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.comul) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom h))
-- Aesop.Saturate
Aesop.saturate : Aesop.LocalRuleSet → Lean.MVarId → Aesop.Options' → Lean.MetaM (Lean.MVarId × Aesop.Stats)
-- Mathlib.Algebra.Order.Archimedean.Defs
MulArchimedean.mk : ∀ {R : Type u_2} [inst : CommMonoid R] [inst_1 : PartialOrder R],
  (∀ (x : R) {y : R}, 1 < y → ∃ n, x ≤ y ^ n) → MulArchimedean R
-- Init.Data.UInt.Bitwise
USize.ofFin_xor : ∀ (a b : Fin USize.size), USize.ofFin (a ^^^ b) = USize.ofFin a ^^^ USize.ofFin b
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_cycleFactorsFinset_support_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {p f : Equiv.Perm α},
  p ∈ f.cycleFactorsFinset → p.support ⊆ f.support