mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Closure
ClosureOperator.mk'_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x)
  (hf₃ : ∀ (x : α), f (f x) ≤ f x) (a : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃) a = f a
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.out : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_monotone : ∀ {V : Type u_1} {W : Type u_2} (f : V → W), Monotone (SimpleGraph.map f)
-- Mathlib.Data.Finsupp.Defs
_private.Mathlib.Data.Finsupp.Defs.0.Finsupp.embDomain.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.beth_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.beth c.ord = c
-- Mathlib.Data.List.Defs
List.map₂Left.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α),
  List.map₂Left f (a :: as) [] = List.map (fun a => f a none) (a :: as)
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.epiWithInjectiveKernel.hasLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  {p : X ⟶ Y},
  CategoryTheory.Abelian.epiWithInjectiveKernel p →
    ∀ {A B : C} (i : A ⟶ B) [CategoryTheory.Mono i], CategoryTheory.HasLiftingProperty i p
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRccSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Rcc.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RccSlice α β)
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_add : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {v₁ v₂ : α →₀ M} {f : α → β},
  Finsupp.mapDomain f (v₁ + v₂) = Finsupp.mapDomain f v₁ + Finsupp.mapDomain f v₂
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.hom_ext_iff : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G}, α = β ↔ ∀ (X : C), α.out.app X = β.out.app X
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_zpow : ∀ {α : Type u_4} {p : α → Prop} (f : Equiv.Perm α) (n : ℤ) (hf : ∀ (x : α), p (f x) ↔ p x),
  f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_two_power : ∀ (a : Cardinal.{u_1}), Cardinal.lift.{v, u_1} (2 ^ a) = 2 ^ Cardinal.lift.{v, u_1} a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec.inj : ∀ {h h_1 : Lean.FVarId},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h = Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h_1 → h = h_1
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_sum_eq_rat : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] [inst_5 : Algebra ℚ 𝔸],
  (NormedSpace.expSeries 𝕂 𝔸).sum = (NormedSpace.expSeries ℚ 𝔸).sum
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.orbitRel_subgroup_le : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (H : Subgroup G),
  MulAction.orbitRel (↥H) α ≤ MulAction.orbitRel G α
-- Lean.Environment
Lean.Environment.instInhabitedVisibility.default : Lean.Environment.Visibility
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.autoImplicitCtx : Array Lean.Expr → Lean.Elab.PartialContextInfo
-- Lean.Environment
Lean.instInhabitedAsyncConstantInfo : Inhabited Lean.AsyncConstantInfo
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitor_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.F =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.Tactic.ITauto
/-- `itauto` solves the main goal when it is a tautology of intuitionistic propositional logic.
Unlike `grind` and `tauto!` this tactic never uses the law of excluded middle (without the `!`
option), and the proof search is tailored for this use case. `itauto` is complete for intuitionistic
propositional logic: it will solve any goal that is provable in this logic.

* `itauto [a, b]` will additionally attempt case analysis on `a` and `b` assuming that it can derive
  `Decidable a` and `Decidable b`.
* `itauto *` will case on all decidable propositions that it can find among the atomic propositions.
* `itauto!` will work as a classical SAT solver, but the algorithm is not very good in this
  situation.
* `itauto! *` will case on all propositional atoms. *Warning:* This can blow up the proof search, so
  it should be used sparingly.

Example:
```lean
example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto
```
 -/
Mathlib.Tactic.ITauto.itauto! : Lean.ParserDescr
-- Std.Time.Time.Unit.Second
/-- Converts an `Ordinal` to an `Second.Offset`.
 -/
Std.Time.Second.Ordinal.toOffset : {leap : Bool} → Std.Time.Second.Ordinal leap → Std.Time.Second.Offset
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ico' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α},
  μ {b} ≠ ⊤ →
    autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ico'._auto_1 →
      (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The isomorphism between `ℤ` and the infinite cyclic group `G` sending
`1` to the generator `g : G`.  -/
intEquivOfZMultiplesEqTop : {G : Type u_2} → [Infinite G] → [inst : AddGroup G] → (g : G) → AddSubgroup.zmultiples g = ⊤ → ℤ ≃+ G
-- Init.Data.BitVec.Lemmas
BitVec.instIsLinearOrder : ∀ {n : ℕ}, Std.IsLinearOrder (BitVec n)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys)
-- Mathlib.Logic.Function.Iterate
Function.iterate_add_eq_iterate : ∀ {α : Type u} {f : α → α} {m n : ℕ} {a : α}, Function.Injective f → (f^[m + n] a = f^[n] a ↔ f^[m] a = a)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] (W X Y Z : C) {Z_1 : D}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.μ F W Y)
          (CategoryTheory.Functor.LaxMonoidal.μ F X Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.μ F W X)
        (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)) h))
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.range_eq_top : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ}, IsCoercive B → (↑(InnerProductSpace.continuousLinearMapOfBilin B)).range = ⊤
-- Mathlib.Analysis.RCLike.Extend
/-- The extension `StrongDual.extendRCLike` as a linear equivalence between the algebraic duals.

When `F` is a normed space, this can be upgraded to an *isometric* linear equivalence, see
`StrongDual.extendRCLikeₗᵢ`.  -/
StrongDual.extendRCLikeₗ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousConstSMul 𝕜 F] →
              [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F ≃ₗ[ℝ] StrongDual 𝕜 F
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.inr_apply : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (x : M₂), (ContinuousLinearMap.inr R M₁ M₂) x = (0, x)
-- Lean.Meta.Sym.Util
/-- Instantiates metavariables and applies `shareCommon`, which maintains the `SymM`
invariants enabled in the current configuration (see `Sym.Config`).
 -/
Lean.Meta.Sym.preprocessExpr : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.liftOn_mk : ∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] {L : Type u_1}
  (f : ℕ × K → L) (hf : ∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y) (x : ℕ × K),
  (PerfectClosure.mk K p x).liftOn f hf = f x
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A braided category with a faithful braided functor to a symmetric category is itself symmetric.
 -/
CategoryTheory.SymmetricCategory.ofFaithful : {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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.SymmetricCategory D] →
                (F : CategoryTheory.Functor C D) → [F.Braided] → [F.Faithful] → CategoryTheory.SymmetricCategory C
-- Mathlib.RingTheory.Localization.Away.Basic
/-- The localization at one is isomorphic to the ring.  -/
IsLocalization.atOne : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization.Away 1 S] → R ≃ₐ[R] S
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Icc_sdiff_Ioo_same`. -/
Set.Icc_diff_Ioo_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Icc a b \ Set.Ioo a b = {a, b}
-- Init.Data.BitVec.Lemmas
/-- Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
because it makes the value of the bitvector less than or equal to `2^(w-1)`.
In the case when `n = 0`, then the shift right value equals the integer interpretation.
 -/
BitVec.toInt_ushiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)
-- Init.Control.MonadAttach
LawfulMonadAttach.canReturn_map_imp : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadAttach m} [self : LawfulMonadAttach m] {α : Type u}
  {P : α → Prop} {x : m (Subtype P)} {a : α}, MonadAttach.CanReturn (Subtype.val <$> x) a → P a
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.ext_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f g : MeasureTheory.Filtration ι m},
  f = g ↔ ↑f = ↑g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {l : List ((a : α) × β a)} {k : α}
  {v : β k}, t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.mk.injEq : ∀ (indName : Lean.Name) (majorPos arity : ℕ) (insterestingCtors : Array Lean.Name) (indName_1 : Lean.Name)
  (majorPos_1 arity_1 : ℕ) (insterestingCtors_1 : Array Lean.Name),
  ({ indName := indName, majorPos := majorPos, arity := arity, insterestingCtors := insterestingCtors } =
      { indName := indName_1, majorPos := majorPos_1, arity := arity_1, insterestingCtors := insterestingCtors_1 }) =
    (indName = indName_1 ∧ majorPos = majorPos_1 ∧ arity = arity_1 ∧ insterestingCtors = insterestingCtors_1)
-- Mathlib.SetTheory.Cardinal.Subfield
Subfield.cardinalMk_closure_le_max : ∀ {α : Type u} (s : Set α) [inst : DivisionRing α],
  Cardinal.mk ↥(Subfield.closure s) ≤ max (Cardinal.mk ↑s) Cardinal.aleph0
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.numAlts : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.ceil_lt_two_mul : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a : K},
  2⁻¹ < a → ↑⌈a⌉₊ < 2 * a
-- Init.Data.String.Basic
String.Slice.Pos.offset_ofSliceTo : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos}, (String.Slice.Pos.ofSliceTo pos).offset = pos.offset
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.Core.norm_eq_zero_iff : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : Norm E], NormedSpace.Core 𝕜 E → ∀ (x : E), ‖x‖ = 0 ↔ x = 0
-- Init.Data.String.Subslice
/-- Creates a `String` from a `Subslice` by copying out the bytes.
 -/
String.Slice.Subslice.toString : {s : String.Slice} → s.Subslice → String
-- Mathlib.Algebra.Regular.ULift
ULift.isRegular_down : ∀ {R : Type v} [inst : Mul R] {a : ULift.{u, v} R}, IsRegular a.down ↔ IsRegular a
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ground.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N),
  f.ground = ⇑(TensorProduct.lid R N) ∘ f.toFun' R ∘ ⇑(TensorProduct.lid R M).symm
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.Raw.getD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → β
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- For the successor structure `succStruct I κ` on `Arrow C ⥤ Arrow C`,
the morphism from an object to its successor induces
morphisms in `C` which consists in attaching `I`-cells.  -/
CategoryTheory.SmallObject.attachCellsOfSuccStructProp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {F G : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)} →
                {φ : F ⟶ G} →
                  (CategoryTheory.SmallObject.succStruct I κ).prop φ →
                    (f : CategoryTheory.Arrow C) →
                      HomotopicalAlgebra.AttachCells I.homFamily (CategoryTheory.Arrow.Hom.left (φ.app f))
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_le_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R}, a ≤ b → ⌊a⌋ ≤ ⌊b⌋
-- Std.Http.Protocol.H1
/-- Handles reader failure state.

On server-side (`.receiving`), it opportunistically emits one error response if
no response head has been sent yet, then closes reader state and records the
failure event/error.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.handleReaderFailed : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle : ∀ {I : Type u} [inst : DecidableEq I] {M : Type u_5} [inst_1 : CommMonoid M] {k l m n : I} {u v : M},
  u ≠ 1 →
    v ≠ 1 →
      (Pi.mulSingle k u * Pi.mulSingle l v = Pi.mulSingle m u * Pi.mulSingle n v ↔
        k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The level for morphisms.  -/
Mathlib.Tactic.Monoidal.Context.level₂ : Mathlib.Tactic.Monoidal.Context → Lean.Level
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)),
  PiTensorProduct.dualDistribInvOfBasis b ∘ₗ PiTensorProduct.dualDistrib = LinearMap.id
-- Mathlib.Analysis.Analytic.Inverse
/-- If an open partial homeomorphism `f` is defined at `a` and has a power series expansion there
with invertible linear term, then `f.symm` has a power series expansion at `f a`, given by the
inverse of the initial power series.  -/
OpenPartialHomeomorph.hasFPowerSeriesAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F},
  a ∈ f.source →
    ∀ {p : FormalMultilinearSeries 𝕜 E F},
      HasFPowerSeriesAt (↑f) p a →
        p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.clear : Lean.MVarId → Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instModule : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                {S : Type u_7} →
                                  [inst_10 : Ring S] →
                                    [inst_11 : Module S W] →
                                      [SMulCommClass R S W] →
                                        [ContinuousConstSMul S W] →
                                          [LinearMap.CompatibleSMul W W S R] → Module S (ContIntertwiningMap π₁ π₂)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.equivOfRightInverse_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁)
  (y : M₂ × ↥(↑f₁).ker), (ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h).symm y = f₂ y.1 + ↑y.2
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_toReal : Measurable ENNReal.toReal
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A],
  autoParam
      (∀ (a : A),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
            (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) =
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
            (CategoryTheory.Functor.commShiftIso F₂ a).hom)
      CategoryTheory.NatTrans.CommShift.shift_comm._autoParam →
    CategoryTheory.NatTrans.CommShift τ A
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instAddCommGroup : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → AddCommGroup (AdicCompletion.AdicCauchySequence I M)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → ∀ (c : F), DifferentiableAt 𝕜 (fun y => f y - c) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_back?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = t.keysArray.back?
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [inst_6 : FaithfulSMul R S],
  IsScalarTower S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)
-- Init.Data.List.Basic
List.Perm.below.trans : ∀ {α : Type u} {motive : (a a_1 : List α) → a.Perm a_1 → Prop} {l₁ l₂ l₃ : List α} (a : l₁.Perm l₂) (a_1 : l₂.Perm l₃),
  List.Perm.below a → motive l₁ l₂ a → List.Perm.below a_1 → motive l₂ l₃ a_1 → List.Perm.below ⋯
-- Batteries.Data.String.Lemmas
/-- The start position of a valid substring is valid.  -/
Substring.Raw.Valid.startValid : ∀ {s : Substring.Raw}, s.Valid → String.Pos.Raw.Valid s.str s.startPos
-- Lean.Elab.Term.TermElabM
/-- Convert an "extra" optional error message into a message `"\n{msg}"` (if `some msg`) and `MessageData.nil` (if `none`)
 -/
Lean.Elab.Term.extraMsgToMsg : Option Lean.MessageData → Lean.MessageData
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` structure on a set defines a `Fintype` structure on its subset.  -/
Set.fintypeSubset : {α : Type u} → (s : Set α) → {t : Set α} → [Fintype ↑s] → [DecidablePred fun x => x ∈ t] → t ⊆ s → Fintype ↑t
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_inv_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.op =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.op X)).hom