mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.head_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (w : List.map f l ≠ []), (List.map f l).head w = f (l.head ⋯)
-- Lean.Elab.Tactic.Omega.Core
/-- Construct the proof term associated to a `tidy` step.  -/
Lean.Elab.Tactic.Omega.Justification.tidyProof : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.unop_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  {f : X ⟶ Y} (φ : W₁.MapFactorizationData W₂ f), φ.unop.p = φ.i.unop
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.inter_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M} (F' : I.Filtration M) [IsNoetherianRing R] [Module.Finite R M], F.Stable → (F' ⊓ F).Stable
-- Mathlib.Algebra.Group.Defs
/-- A commutative group is a group with commutative `(*)`. 

[Wikidata Q181296](https://www.wikidata.org/wiki/Q181296) -/
CommGroup : Type u → Type u
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- This lemma is useful in the manifold library in the case that `e` is a chart. It states that
locally around `e x` the set `e.symm ⁻¹' s` is the same as the set intersected with the target
of `e` and some other neighborhood of `f x` (which will be the source of a chart on `Z`).  -/
OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z},
  ContinuousWithinAt f s x →
    x ∈ e.source → t ∈ nhds (f x) → ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
-- Mathlib.Tactic.Translate.Core
/-- A hint about the translated declaration

- `existing` indicates that the translated form of the declaration is a pre-existing declaration.
This is useful when the value cannot be translated, either because of a limitation in the
translation heuristics, or because the value/proof is genuinely different.

- `self` indicates that the declaration translates to itself, up to some reordering of arguments.
If no arguments are reordered then the attribute is redundant, which the `translateRedundant`
linter will warn about.

- `none` indicates that the translated declaration should not get a user-facing name,
instead being named like an auxiliary declaration. This is particularly useful for `to_dual` when
using the `reassoc` attribute, because the dual of a right associated term is left associated,
but we only want user-facing lemmas with right associated terms.
 -/
Mathlib.Tactic.Translate.translationHint : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.instInhabitedExpr.default : Int.Internal.Linear.Expr
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.toTopologicalSpace_injective : ∀ {R : Type u_1} [inst : Ring R], Function.Injective RingTopology.toTopologicalSpace
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (i₁ i₂ : E.I₀)
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)],
  E.sieve₁' i₁ i₂ = CategoryTheory.Sieve.ofArrows E.Y fun j => E.toPullback j
-- Init.Data.Ord.UInt
UInt32.instTransOrd : Std.TransOrd UInt32
-- Init.Grind.Ordered.Ring
/-- In a strict ordered semiring, we can multiply an inequality `a < b` on the right
by a positive element `0 < c` to obtain `a * c < b * c`.  -/
Lean.Grind.OrderedRing.mul_lt_mul_of_pos_right : ∀ {R : Type u} {inst : Lean.Grind.Semiring R} {inst_1 : LE R} {inst_2 : LT R} {inst_3 : Std.IsPreorder R}
  [self : Lean.Grind.OrderedRing R] {a b c : R}, a < b → 0 < c → a * c < b * c
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Like `mapDomain_zero`, but for the `1` we define in this file  -/
SkewMonoidAlgebra.mapDomain_one : ∀ {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [inst : Semiring β] [inst_1 : Monoid α]
  [inst_2 : Monoid α₂] [inst_3 : FunLike F α α₂] [MonoidHomClass F α α₂] (f : F), (SkewMonoidAlgebra.mapDomain ⇑f) 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.toSubgraph.isSpanning : ∀ {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G), (SimpleGraph.toSubgraph H h).IsSpanning
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_inv : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (σ : Equiv.Perm α), σ⁻¹.support = σ.support
-- Mathlib.Order.Lattice
le_sup_of_le_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → Std.DHashMap.Raw.Const.insertMany m [] = m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_coe_pi : -↑Real.pi = ↑Real.pi
-- Mathlib.Data.Set.Operations
Set.apply_rangeSplitting : ∀ {α : Type u} {β : Type v} (f : α → β) (x : ↑(Set.range f)), f (Set.rangeSplitting f x) = ↑x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_Option_lift : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {e : ε} [inst : Std.Do.WP m ps]
  [inst_1 : MonadExceptOf ε m] (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp (MonadExceptOf.throw e)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)⦄
    MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.Order.Defs.LinearOrder
ne_iff_lt_or_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≠ b ↔ a < b ∨ b < a
-- Init.Data.Array.Attach
Array.pmap_eq_self : ∀ {α : Type u_1} {xs : Array α} {p : α → Prop} {hp : ∀ a ∈ xs, p a} {f : (a : α) → p a → α},
  Array.pmap f xs hp = xs ↔ ∀ (a : α) (h : a ∈ xs), f a ⋯ = a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.apply_one : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (x : X), F (1, x) = f₁ x
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- A complete equipartite subgraph in `r > 0` parts each of size `t ≠ 0` in `G` is `r` subsets
of vertices each of size `t` such that vertices in distinct subsets are adjacent.

If `r > 0` but `t = 0`, then `parts = {{}}`. If `r = 0`, then `parts = {}`. These are the two
*distinct* "empty" complete equipartite subgraphs, that is, the complete equipartite subgraphs
having no vertices.  -/
SimpleGraph.CompleteEquipartiteSubgraph : {V : Type u_1} → SimpleGraph V → ℕ → ℕ → Type u_1
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.noConfusionType : Sort v✝ → Lean.Elab.RecKind → Lean.Elab.RecKind → Sort v✝
-- Std.Time.DateTime
/-- Getter for the `Day` inside of a `DateTime`
 -/
Std.Time.DateTime.day : Std.Time.DateTime → Std.Time.Day.Ordinal
-- Mathlib.Order.Minimal
maximal_iff_maximal_of_imp_of_forall : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : PartialOrder α],
  (∀ ⦃x : α⦄, Q x → P x) → (∀ ⦃x : α⦄, P x → ∃ y, x ≤ y ∧ Q y) → (Maximal P x ↔ Maximal Q x)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.mk.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f : A} {d d_1 : ι} (e_d : d = d_1) (hf : f ∈ 𝒜 d) (n n_1 : ℕ) (e_n : n = n_1) (x x_1 : A)
  (e_x : x = x_1) (hx : x ∈ 𝒜 (n • d)),
  HomogeneousLocalization.Away.mk 𝒜 hf n x hx = HomogeneousLocalization.Away.mk 𝒜 ⋯ n_1 x_1 ⋯
-- Init.Data.NeZero
NeZero.ne : ∀ {R : Type u_1} [inst : Zero R] (n : R) [h : NeZero n], n ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The set of common neighbors between two vertices `v` and `w` in a graph `G` is the
intersection of the neighbor sets of `v` and `w`.  -/
SimpleGraph.commonNeighbors : {V : Type u} → SimpleGraph V → V → V → Set V
-- Mathlib.Algebra.Group.Defs
neg_zero : ∀ {G : Type u_1} [inst : NegZeroClass G], -0 = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.keyword : Lean.Lsp.CompletionItemKind
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanShapeEnd_L : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J], (CategoryTheory.Limits.multicospanShapeEnd J).L = J
-- Init.Data.List.Nat.Modify
List.eraseIdx_modifyHead_of_pos : ∀ {α : Type u_1} {f : α → α} {l : List α} {i : ℕ},
  0 < i → (List.modifyHead f l).eraseIdx i = List.modifyHead f (l.eraseIdx i)
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.postComp_a : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z Z' : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (h : Z ⟶ Z'),
  (f.postComp h).a = CategoryTheory.CategoryStruct.comp f.a h
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.RingTheory.Finiteness.Finsupp
LinearMap.finsuppLinearMap_bijective_of_moduleFinite : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (S : Type u_5) [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] [Module.Finite R M],
  Function.Bijective ⇑(LinearMap.finsuppLinearMap S)
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.compl_compl : ∀ {R : Type u_1} [inst : NonAssocRing R] (a : { a // IsIdempotentElem a }), aᶜᶜ = a
-- Lean.Elab.Eval
Lean.Elab.Term.evalTerm : (α : Type) → Lean.Expr → Lean.Syntax → optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe → Lean.Elab.TermElabM α
-- Mathlib.Data.List.Basic
List.length_eq_length_filter_add : ∀ {α : Type u} {l : List α} (f : α → Bool), l.length = (List.filter f l).length + (List.filter (fun x => !f x) l).length
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t ∈ ∂𝒜` iff `t` is exactly one element less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_mem_card_add_one`.  -/
Finset.mem_shadow_iff_exists_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mkOfAdjoinEqTop'_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Module.Finite R S] [inst_4 : Module.Free R S] {α : S} (hα : R[α] = ⊤),
  (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = Polynomial.aeval α
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.HasOfPostcompProperty W'], W.op.HasOfPrecompProperty W'.op
-- Lean.Compiler.ExternAttr
Lean.expandExternPattern : String → List String → String
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousVAdd.finite_stabilizer : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
  [ProperlyDiscontinuousVAdd Γ T] (x : T), (↑(AddAction.stabilizer Γ x)).Finite
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel_not_epi_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f],
  f ≠ 0 → ¬CategoryTheory.Epi (CategoryTheory.Limits.kernel.ι f)
-- Mathlib.Topology.ShrinkingLemma
/-- The set of indexes `i` such that `i`-th set is already shrunk.  -/
ShrinkingLemma.PartialRefinement.carrier : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} → {s : Set X} → {p : Set X → Prop} → ShrinkingLemma.PartialRefinement u s p → Set ι
-- Lean.Meta.Tactic.Grind.EqResolution
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.topsortMVars?.visitTypeOf : Array Lean.Expr → Lean.Expr → Lean.Meta.Grind.TopSortM Unit
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is `gt` or `eq`.
 -/
Ordering.isGE : Ordering → Bool
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.isAlgebraic_tower_bot : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  [Algebra.IsAlgebraic K L], Algebra.IsAlgebraic K ↥S
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The coherent coverage on a precoherent category `C`.
 -/
CategoryTheory.coherentCoverage : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Precoherent C] → CategoryTheory.Coverage C
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.instT0Space : ∀ {α : Type u_1} [inst : UniformSpace α], T0Space (TopologicalSpace.Closeds α)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G] (x : C × C),
  (CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting F G).app x =
    CategoryTheory.CategoryStruct.comp (β_ ((G, F).2.obj x.2) ((G, F).1.obj x.1)).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x.2, x.1))
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map (β_ (x.2, x.1).2 (x.2, x.1).1).inv))
-- Mathlib.FieldTheory.Differential.Liouville
IsLiouville.mk : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K],
  (∀ (a : F) (ι : Type) [inst_5 : Fintype ι] (c : ι → F),
      (∀ (x : ι), (c x)′ = 0) →
        ∀ (u : ι → K) (v : K),
          ↑a = ∑ x, ↑(c x) * Differential.logDeriv (u x) + v′ →
            ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * Differential.logDeriv (u₀ x) + v₀′) →
    IsLiouville F K
-- Mathlib.FieldTheory.Differential.Basic
Differential.instDifferentialAlgebraAdjoinRoot : ∀ {F : Type u_2} [inst : Field F] [inst_1 : Differential F] [inst_2 : CharZero F] (p : Polynomial F)
  [inst_3 : Fact (Irreducible p)] [inst_4 : Fact p.Monic], DifferentialAlgebra F (AdjoinRoot p)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_mul_denom_add_denom_mul_num_ne_zero : ∀ {K : Type u} [inst : Field K] {x y : RatFunc K}, x + y ≠ 0 → x.num * y.denom + x.denom * y.num ≠ 0
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_apply_linear_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p : P), (↑((signedDist v) p)).linear w = inner ℝ (NormedSpace.normalize v) w
-- Mathlib.Order.Completion
/-- The Dedekind-MacNeille completion of a partial order is the smallest complete lattice containing
it, in the sense that any embedding into any complete lattice factors through it.  -/
DedekindCut.principalEmbedding_trans_factorEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : PartialOrder β] (f : β ↪o α),
  RelEmbedding.trans DedekindCut.principalEmbedding (DedekindCut.factorEmbedding f) = f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- A localization map between monoids automatically preserves 1 and therefore
is a monoid homomorphism.  -/
Submonoid.LocalizationMap.toMonoidHom : {M : Type u_1} →
  [inst : CommMonoid M] → {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → M →* N
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lflip_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {R₀ : Type u_14} [inst_12 : Semiring R₀] [inst_13 : Module R₀ P] [inst_14 : SMulCommClass S₂ R₀ P]
  [inst_15 : SMulCommClass R₂ R₀ P], LinearMap.lflip.symm = LinearMap.lflip
-- Init.Data.SInt.Lemmas
Int16.not_lt : ∀ {a b : Int16}, ¬a < b ↔ b ≤ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.forIn_eq_forIn_toArray : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn f init t =
    forIn (Std.DTreeMap.Internal.Impl.Const.toArray t) init fun a b => f a.1 a.2 b
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C (CategoryTheory.CommMon D)) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.map f = (F.map f).hom.hom
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat : ∀ (X : CondensedSet), UCompactlyGeneratedSpace ↑(condensedSetToTopCat.obj X)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  (↑m).WF → ∀ {a : α}, m.contains a = true → m.getKey? a = some a
-- Lean.Elab.Do.Basic
/-- Return `$e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k)`, cancelling
the bind if `$(← dec.k)` is `pure $dec.resultName` or `e` is some `pure` computation.
 -/
Lean.Elab.Do.DoElemCont.mkBindUnlessPure : Lean.Elab.Do.DoElemCont → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.RingTheory.IsAdjoinRoot
Algebra.adjoin.powerBasis'_minpoly_gen : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsDomain S] [inst_5 : Module.IsTorsionFree R S] [inst_6 : IsIntegrallyClosed R] {x : S}
  (hx' : IsIntegral R x), minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.liftRingHom_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
  (f :
    { f //
      f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }),
  DirectSum.liftRingHom f = DirectSum.toSemiring (fun x => ↑f) ⋯ ⋯
-- Mathlib.NumberTheory.Padics.AddChar
/-- Equivalence between continuous additive characters `ℤ_[p] → R`, and `r ∈ R` with `r ^ n → 0`.  -/
PadicInt.continuousAddCharEquiv : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (R : Type u_1) →
      [inst_1 : NormedRing R] →
        [inst_2 : Algebra ℤ_[p] R] →
          [IsBoundedSMul ℤ_[p] R] →
            [IsUltrametricDist R] →
              [CompleteSpace R] →
                { κ // Continuous ⇑κ } ≃ { r // Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0) }
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsIntegralHom f],
  AlgebraicGeometry.IsIntegralHom (f ∣_ V)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_bot : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  Subsemiring.map f ⊥ = ⊥
-- Batteries.Data.AssocList
Batteries.AssocList.eraseP.eq_def : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (x : Batteries.AssocList α β),
  Batteries.AssocList.eraseP p x =
    match x with
    | Batteries.AssocList.nil => Batteries.AssocList.nil
    | Batteries.AssocList.cons k v es =>
      bif p k v then es else Batteries.AssocList.cons k v (Batteries.AssocList.eraseP p es)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.hasEqualizer_of_common_retraction : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoreflexiveEqualizers C] {A B : C}
  {f g : A ⟶ B} (r : B ⟶ A),
  CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id A →
    CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.id A → CategoryTheory.Limits.HasEqualizer f g
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- We have `c * φ = Φ` as polynomials with coefficients in `Ratfunc K`. See Equation
(11.3.5) in Cohn's proof.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.C_c_mul_φ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ →
    Polynomial.C (RatFunc.Luroth.c✝ E) * Polynomial.map (algebraMap (↥E) (RatFunc K)) (RatFunc.Luroth.φ✝ E) =
      Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.Φ✝ E)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a a_1 : W ⟶ Y) (e_a : a = a_1) (b b_1 : W ⟶ Z)
  (e_b : b = b_1) (h : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
  CategoryTheory.ChosenPullbacksAlong.lift a b h = CategoryTheory.ChosenPullbacksAlong.lift a_1 b_1 ⋯
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
-- Init.Data.UInt.Lemmas
UInt8.mul_neg : ∀ (a b : UInt8), a * -b = -(a * b)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addGroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddGroup β],
  e.addGroup = Function.Injective.addGroup ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Finset.Sym
Finset.injective_sym2 : ∀ {α : Type u_1}, Function.Injective Finset.sym2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.leftUnitor_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.le_iff_of_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι] [inst_2 : Unique ι]
  [inst_3 : (i : ι) → PartialOrder (α i)] {x y : Lex (Π₀ (i : ι), α i)}, x ≤ y ↔ (ofLex x) default ≤ (ofLex y) default