mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The linear isometry equivalence version of `TensorProduct.assoc`.  -/
TensorProduct.assocIsometry : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      (G : Type u_4) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] →
                      TensorProduct 𝕜 (TensorProduct 𝕜 E F) G ≃ₗᵢ[𝕜] TensorProduct 𝕜 E (TensorProduct 𝕜 F G)
-- Mathlib.Order.Filter.Lift
Filter.lift_mono' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g₁ g₂ : Set α → Filter β},
  (∀ s ∈ f, g₁ s ≤ g₂ s) → f.lift g₁ ≤ f.lift g₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.DTreeMap.Raw.ofList l cmp).getKey? k' = some k
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverMincard_closure_le : ∀ {X : Type u_1} {T : X → X} {V : SetRel X X} [inst : UniformSpace X],
  Continuous T →
    ∀ (F : Set X) (U : SetRel X X),
      V ∈ uniformity X → ∀ (n : ℕ), Dynamics.coverMincard T (closure F) (V.comp U) n ≤ Dynamics.coverMincard T F U n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.bind_subtypeCasesOn'_eq_map_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop} (x : m (Subtype P))
  (f : α → m β),
  (do
      let a ← x
      Std.Internal.subtypeCasesOn'✝ a fun a x => f a) =
    Subtype.val <$> x >>= f
-- Mathlib.Order.ScottContinuity
scottContinuousOn_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  ScottContinuousOn Set.univ f ↔ ScottContinuous f
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_eq_four : ∀ {α : Type u_1} {v : FreeAddMonoid α},
  v.length = 4 ↔ ∃ a b c d, v = FreeAddMonoid.of a + FreeAddMonoid.of b + FreeAddMonoid.of c + FreeAddMonoid.of d
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c_1 → c = c_1
-- Mathlib.Combinatorics.Graph.Lattice
Graph.inf_isLoopAt_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  (G ⊓ H).IsLoopAt e x ↔ G.IsLoopAt e x ∧ H.IsLoopAt e x
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- The counit of the equivalence we're constructing.  -/
CategoryTheory.OverPresheafAux.counit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).comp
          (CategoryTheory.OverPresheafAux.restrictedYoneda A) ≅
        CategoryTheory.Functor.id
          (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
-- Mathlib.Logic.Equiv.List
Denumerable.list_ofNat_zero : ∀ {α : Type u_1} [inst : Denumerable α], Denumerable.ofNat (List α) 0 = []
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.num_mem_deg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f : HomogeneousLocalization 𝒜 x), f.num ∈ 𝒜 f.deg
-- Init.Util
/-- Compares two lists of objects for element-wise pointer equality. Returns `true` if both lists are
the same length and the objects at the corresponding indices of each list are pointer-equal.

Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This
function is unsafe because it can distinguish between definitionally equal values.
 -/
ptrEqList : {α : Type u_1} → List α → List α → Bool
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The left morphism of the fork diagram.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.forkMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type t} →
          [inst_1 : Small.{w, t} I] →
            (X : I → C) →
              ((i : I) → X i ⟶ B) → (P.obj (Opposite.op B) ⟶ CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X)
-- Mathlib.Algebra.Module.Basic
Function.support_smul_subset_left : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (f : α → R)
  (g : α → M), Function.support (f • g) ⊆ Function.support f
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The additive units of `S`, packaged as an additive subgroup of `AddUnits M`.  -/
AddSubmonoid.addUnits : {M : Type u_1} → [inst : AddMonoid M] → AddSubmonoid M → AddSubgroup (AddUnits M)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder.eq_3 : ∀ (n : ℕ), (n = 0 → False) → n.succ.smallSchroder = n.largeSchroder / 2
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A weakly regular sequence `rs` on `M` is regular if also `M/rsM ≠ 0`.  -/
RingTheory.Sequence.IsRegular : {R : Type u_1} → (M : Type u_3) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → List R → Prop
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange f).inv f =
    (AlgebraicGeometry.Scheme.Hom.opensRange f).ι
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.dist_le_dist_pi_of_dist_lt : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → PseudoMetricSpace (F i)]
  {x y : (i : ι) → F i} {i : ι}, dist x y < 2⁻¹ ^ Encodable.encode i → dist (x i) (y i) ≤ dist x y
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeSet_replaceVertex_of_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V],
  G.Adj s t →
    (G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.prod_fst_snd : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B],
  (NonUnitalAlgHom.fst R A B).prod (NonUnitalAlgHom.snd R A B) = 1
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binSearchAux.match_1.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (x : Fin (as.size + 1)) → (x_1 : Fin as.size) → ↑x ≤ ↑x_1 → Sort u_2)
  (lo : Fin (as.size + 1)) (hi : Fin as.size) (h : ↑lo ≤ ↑hi)
  (h_1 : (lo : Fin (as.size + 1)) → (hi : Fin as.size) → (h : ↑lo ≤ ↑hi) → motive lo hi h),
  (match lo, hi, h with
    | lo, hi, h => h_1 lo hi h) =
    h_1 lo hi h
-- Mathlib.AlgebraicGeometry.Scheme
/-- We give schemes the specialization preorder by default.
 -/
AlgebraicGeometry.Scheme.instPreorderCarrierCarrierCommRingCat : {X : AlgebraicGeometry.Scheme} → Preorder ↥X
-- Mathlib.Data.Nat.Nth
Nat.isLeast_nth_of_lt_card : ∀ {p : ℕ → Prop} {n : ℕ} (hf : (Set.ofPred p).Finite),
  n < hf.toFinset.card → IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The quotient of the unit group of `A` by the principal unit group of `A` agrees with
the units of the residue field of `A`.  -/
ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits : {K : Type u} →
  [inst : Field K] →
    (A : ValuationSubring K) →
      ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃* (IsLocalRing.ResidueField ↥A)ˣ
-- Init.Data.Array.Lemmas
Array.mem_append : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- When the domain is a real normed space, `ContinuousLinearMap.sSup_unitClosedBall_eq_norm` can be
tightened to take the supremum over only the `Metric.sphere`.  -/
ContinuousLinearMap.sSup_sphere_eq_norm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜]
  (f : E →SL[σ₁₂] F), sSup ((fun x => ‖f x‖) '' Metric.sphere 0 1) = ‖f‖
-- Mathlib.Data.EReal.Basic
EReal.natCast_eq_iff : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
-- Mathlib.Data.Seq.Computation
Computation.bind_congr : ∀ {α : Type u} {β : Type v} {s1 s2 : Computation α} {f1 f2 : α → Computation β},
  s1.Equiv s2 → (∀ (a : α), (f1 a).Equiv (f2 a)) → (s1.bind f1).Equiv (s2.bind f2)
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density is unaffected by removing `0`.  -/
schnirelmannDensity_sdiff_singleton_zero : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ A \ {0}],
  schnirelmannDensity (A \ {0}) = schnirelmannDensity A
-- Std.Data.TreeMap.Raw.Iterator
/-- Returns a finite iterator over the entries of a tree map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.Raw.iter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.Iter (α × β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Mathlib.Topology.Inseparable
SeparationQuotient.mk_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : One X], SeparationQuotient.mk 1 = 1
-- Mathlib.Algebra.Group.AddChar
AddChar.mulShift_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] {ψ : AddChar R M} {r x : R},
  (ψ.mulShift r) x = ψ (r * x)
-- Mathlib.Probability.Martingale.Convergence
/-- **Lévy's upward theorem**, almost everywhere version: given a function `g` and a filtration
`ℱ`, the sequence defined by `𝔼[g | ℱ n]` converges almost everywhere to `𝔼[g | ⨆ n, ℱ n]`.  -/
MeasureTheory.tendsto_ae_condExp : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ),
  ∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun n => μ[g | ↑ℱ n] x) Filter.atTop (nhds (μ[g | ⨆ n, ↑ℱ n] x))
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.packingRadius_lt_dist_of_mem_ne : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) {x y : X},
  x ∈ D → y ∈ D → x ≠ y → ↑D.packingRadius < dist x y
-- Mathlib.Algebra.Module.Equiv.Basic
Module.End.isUnit_iff : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M), IsUnit f ↔ Function.Bijective ⇑f
-- Mathlib.Algebra.BrauerGroup.Defs
CSA.mk : {K : Type u} →
  [inst : Field K] →
    (toAlgCat : AlgCat K) →
      [isCentral : Algebra.IsCentral K ↑toAlgCat] →
        [isSimple : IsSimpleRing ↑toAlgCat] → [fin_dim : FiniteDimensional K ↑toAlgCat] → CSA K
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.monotone_intro : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  Monotone u → Monotone l → (∀ (a : α), a ≤ u (l a)) → (∀ (a : β), l (u a) ≤ a) → GaloisConnection l u
-- Mathlib.Topology.EMetricSpace.Defs
WeakEMetricSpace.eq_of_edist_eq_zero : ∀ {α : Type u} {inst : TopologicalSpace α} [self : WeakEMetricSpace α] {x y : α}, edist x y = 0 → x = y
-- Lean.Compiler.IR.Basic
Lean.IR.addParamsRename : Lean.IR.IndexRenaming → Array Lean.IR.Param → Array Lean.IR.Param → Option Lean.IR.IndexRenaming
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instFiniteEdgeLabelingOfElemSym2EdgeSet : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Finite ↑G.edgeSet] [Finite K], Finite (G.EdgeLabeling K)
-- Mathlib.Topology.Path
Path.instContinuousEvalElemRealUnitInterval : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ContinuousEval (Path x y) (↑unitInterval) X
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.mk.injEq : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} (marks : Array Bool) (hmarks : marks.size = aig.decls.size)
  (inv : Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks hmarks) (marks_1 : Array Bool)
  (hmarks_1 : marks_1.size = aig.decls.size) (inv_1 : Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf marks_1 hmarks_1),
  ({ marks := marks, hmarks := hmarks, inv := inv } = { marks := marks_1, hmarks := hmarks_1, inv := inv_1 }) =
    (marks = marks_1)
-- Mathlib.Tactic.Nontriviality.Core
/-- `nontriviality α` generates a proof of `Nontrivial α` and adds this as a hypothesis.

The tactic first tries to find a proof of `Nontrivial α` using instance synthesis.
If this fails, it will derive this proof using `a < b`, `a ≠ b` or `a > b` hypotheses in the
local context. Otherwise it will perform a case split on `Subsingleton α ∨ Nontrivial α`, and
attempt to prove `Subsingleton α` implies the main goal using `simp [nontriviality]`.
If the `Subsingleton` goal cannot be closed automatically, `nontriviality` fails.

This tactic is extensible: tag a lemma with `@[nontriviality]` to use it in the `simp` set for the
`Subsingleton` case. All `@[simp]` lemmas are automatically used too.

* `nontriviality` (without the argument `α`) infers the type from the main goal,
  if the goal is an (in)equality.
* `nontriviality using h₁, h₂, ..., hₙ` uses `h₁`, ..., `hₙ` as extra arguments to `simp`
  in the `Subsingleton` case. This supports the typical `simp` argument syntax:
  `nontriviality using ← h` rewrites right-to-left with this argument;
  `nontriviality using -h` removes a lemma from the default `simp` set for this tactic invocation.
  `nontriviality using *` adds all local hypotheses to the `simp` set.

Examples:
```
example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  assumption

example {R : Type} [CommRing R] {r s : R} : r * s = s * r := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  apply mul_comm

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 := by
  nontriviality R -- there is now a `Nontrivial R` hypothesis available.
  dec_trivial

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b := by
  success_if_fail nontriviality α -- Fails
  nontriviality α using myeq -- There is now a `Nontrivial α` hypothesis available
  assumption
```
 -/
Mathlib.Tactic.Nontriviality.nontriviality : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a : α}, ∅.getKey? a = none
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequenceProp_inl_none : ∀ (o : ONote), o.FundamentalSequenceProp (Sum.inl none) ↔ o = 0
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_union : ∀ (x y : ZFSet.{u_1}), (x ∪ y).rank = max x.rank y.rank
-- Std.Async.System
Std.Async.System.GroupId.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompLinearEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W]
  (p : W × (V →L[R] W)) (x : V), ((ContinuousAffineMap.decompLinearEquiv R S V W).symm p) x = p.2 x + p.1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsScalarTower : ∀ {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F]
  [inst_10 : SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' F], IsScalarTower 𝕜 𝕜' (SchwartzMap E F)
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree : Type
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.exp_mul : ∀ (x : EReal) (y : ℝ), (x * ↑y).exp = x.exp ^ y
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a b : α i), Function.update f i '' Set.Ioc a b = Set.Ioc (Function.update f i a) (Function.update f i b)
-- Mathlib.Data.Set.Image
Set.image_eq_preimage_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.LeftInverse g f → Function.RightInverse g f → Set.image f = Set.preimage g
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.of_sSup_simples_eq_top : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  sSup {m | IsSimpleModule R ↥m} = ⊤ → IsSemisimpleModule R M
-- Mathlib.Logic.Hydra
Relation.cutExpand_double : ∀ {α : Type u_1} {r : α → α → Prop} {a a₁ a₂ : α}, r a₁ a → r a₂ a → Relation.CutExpand r {a₁, a₂} {a}
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {a : IsDedekindDomain.FiniteAdeleRing R K},
  (∀ (v : IsDedekindDomain.HeightOneSpectrum R), a v ≠ 0) → ¬IsUnit a → {v | Valued.v (a v) ≠ 1}.Infinite
-- Init.Data.List.Zip
List.zip_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {l : List α},
  (List.map f l).zip (List.map g l) = List.map (fun a => (f a, g a)) l
-- Mathlib.Order.RelSeries
LTSeries.head_le : ∀ {α : Type u_1} [inst : Preorder α] (x : LTSeries α) (n : Fin (x.length + 1)), RelSeries.head x ≤ x.toFun n
-- Mathlib.Order.SuccPred.InitialSeg
/-- **Alias** of the reverse direction of `PrincipalSeg.isSuccPrelimit_apply_iff`. -/
PrincipalSeg.map_isSuccPrelimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  Order.IsSuccPrelimit a → Order.IsSuccPrelimit (f.toRelEmbedding a)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.isCompact_closure_image_closedBall : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → ∀ (r : ℝ), IsCompact (closure (⇑f '' Metric.closedBall 0 r))
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_map_symm : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (I : FractionalIdeal S P) (g : P ≃ₐ[R] P'),
  FractionalIdeal.map (↑g.symm) (FractionalIdeal.map (↑g) I) = I
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExp_set_generateFrom_singleton : ∀ {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      μ[t.indicator fun ω => 1 | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x => μ[|s].real t
-- Std.Sync.Mutex
/-- Waits on the condition variable until the predicate is true.  -/
Std.Condvar.waitUntil : {m : Type → Type u_1} → [Monad m] → [MonadLiftT BaseIO m] → Std.Condvar → Std.BaseMutex → m Bool → m Unit
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRocSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Roc.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RocSlice α β)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi'_δ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).Monoidal] (X Y : D) (i : I),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.pi' F) X Y i =
    CategoryTheory.Functor.OplaxMonoidal.δ (F i) X Y
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The preimage of the normalizer is equal to the normalizer of the preimage of
a surjective function.  -/
AddSubgroup.comap_normalizer_eq_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : N →+ G},
  Function.Surjective ⇑f →
    AddSubgroup.comap f (AddSubgroup.normalizer ↑H) = AddSubgroup.normalizer ↑(AddSubgroup.comap f H)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_coe' : ∀ {α : Type u_1} (n : ℕ) (l : List α), Multiset.powersetCard n ↑l = ↑(Multiset.powersetCardAux n l)
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `none` if no such element exists.
 -/
Std.ExtTreeSet.getGT? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Option α
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.sdiff_subset_loops_contract : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → X \ I ⊆ (M.contract I).loops
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableOn_atlas_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H} [IsManifold I 1 M],
  e ∈ atlas H M → MDiff[e.target] ↑e.symm
-- Mathlib.Order.Bounds.Basic
isLeast_hnot : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), IsLeast {w | Codisjoint a w} (￢a)
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasLimitsOfShape_skeleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Skeleton C)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.symm : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {x : MeasurableSpace β}
  {x_1 : MeasurableSpace β'}, ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun g f κ μ