mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_div : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The multiplication on the graded tensor product.

See `GradedTensorProduct.coe_mul_coe` for a characterization on pure tensors.  -/
GradedTensorProduct.instMul : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → [Module ι (Additive ℤˣ)] → Mul (GradedTensorProduct R 𝒜 ℬ)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsRightKanExtensionObjRanAppRanCounit : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H),
  (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α), (Stream'.WSeq.cons a s).tail = s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [Inhabited α] {k fallback : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α}
  [inst_3 : Inhabited (β a)], ∅.get! a = default
-- Mathlib.Data.Int.GCD
Nat.xgcdAux_val : ∀ (x y : ℕ), x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
-- Mathlib.Data.Stream.Init
Stream'.tail_map : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α), (Stream'.map f s).tail = Stream'.map f s.tail
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold_cons : ∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α) (a : α)
  (h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => op x y = op y x) (h' : {x | x ∈ s}.Pairwise fun x y => op x y = op y x)
  (x : α), Multiset.noncommFold op (a ::ₘ s) h x = op a (Multiset.noncommFold op s h' x)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.insert k).get! a = if (k == a) = true ∧ k ∉ m then k else m.get! a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  K.cyclesIsoSc' i j k hi hk = K.cyclesIsoSc' i j k hi hk
-- Mathlib.Topology.Homotopy.Lifting
IsLocalHomeomorph.continuous_lift : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X},
  IsLocalHomeomorph p →
    IsSeparatedMap p →
      ∀ (f : C(↑unitInterval × A, X)) {g : ↑unitInterval × A → E},
        p ∘ g = ⇑f → (Continuous fun x => g (0, x)) → (∀ (a : A), Continuous fun x => g (x, a)) → Continuous g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.Data.Finsupp.Basic
Finsupp.embDomain_eq_mapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α ↪ β) (v : α →₀ M),
  Finsupp.embDomain f v = Finsupp.mapDomain (⇑f) v
-- Init.Data.List.Lemmas
List.mem_cons : ∀ {α : Type u_1} {b : α} {l : List α} {a : α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G),
  CategoryTheory.Presheaf.IsLocallySurjective J f ↔
    CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range f) = ⊤
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instAddCommMonoid : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → AddCommMonoid (CentroidHom α)
-- Init.Data.Array.Subarray
Subarray.start.eq_1 : ∀ {α : Type u_1} (xs : Subarray α), xs.start = xs.internalRepresentation.start
-- Mathlib.Data.Set.Order
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright.  -/
Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_X : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (i : σ), MvPolynomial.constantCoeff (MvPolynomial.X i) = 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {k : α},
  m.WF → m.toArray.contains k = m.contains k
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
 -/
CategoryTheory.NatIso.pi : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          {F G : (i : I) → CategoryTheory.Functor (C i) (D i)} →
            ((i : I) → F i ≅ G i) → (CategoryTheory.Functor.pi F ≅ CategoryTheory.Functor.pi G)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instCoeOutRingComputeRingCompare : {u : Lean.Level} →
  {α : Q(Type u)} →
    (BaseType : Q(«$α») → Type) →
      (sα : Q(CommSemiring «$α»)) →
        CoeOut (Mathlib.Tactic.Ring.Common.RingCompute BaseType sα) (Mathlib.Tactic.Ring.Common.RingCompare BaseType)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mem_ker_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {p : Polynomial R}, p ∈ RingHom.ker h.map ↔ f ∣ p
-- Mathlib.Algebra.GroupWithZero.Defs
/-- For all `a` and `b` of `M₀`, `a * b = 0` implies `a = 0` or `b = 0`.  -/
NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {M₀ : Type u_2} {inst : Mul M₀} {inst_1 : Zero M₀} [self : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.trans_fst : ∀ {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁) (G : TopPair.Homotopy f₁ f₂),
  (F.trans G).fst = F.fst.trans G.fst
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.mk.injEq : ∀ (lhs rhs : Lean.Grind.AC.Seq) (h : Lean.Meta.Grind.AC.DiseqCnstrProof) (lhs_1 rhs_1 : Lean.Grind.AC.Seq)
  (h_1 : Lean.Meta.Grind.AC.DiseqCnstrProof),
  ({ lhs := lhs, rhs := rhs, h := h } = { lhs := lhs_1, rhs := rhs_1, h := h_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ h = h_1)
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.eraseMany : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.TreeSet.Raw α cmp}, t.WF → (t.eraseMany l).WF
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_biUnion_lt_top : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α},
  s.Finite → (∀ i ∈ s, μ (f i) < ⊤) → μ (⋃ i ∈ s, f i) < ⊤
-- Mathlib.RingTheory.Flat.Basic
LinearMap.rTensor_injective_of_fg : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] {f : N →ₗ[R] P},
  (∀ (N' : Submodule R N) (P' : Submodule R P),
      N'.FG → P'.FG → ∀ (h : N' ≤ Submodule.comap f P'), Function.Injective ⇑(LinearMap.rTensor M (f.restrict h))) →
    Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.Order.Bounds.Basic
IsLeast.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  IsLeast s a → IsGreatest (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The `ωSup` operator for monotone functions.  -/
OmegaCompletePartialOrder.OrderHom.ωSup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → OmegaCompletePartialOrder.Chain (α →o β) → α →o β
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) ((fun₀ | (g, g⁻¹) => (A.ρ g) a) - fun₀ | (g⁻¹, g) => a) =
    (fun₀ | 1 => a) - fun₀ | 1 => (A.ρ g) a
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep : (s : String.Slice) → Std.Iterator (String.Slice.Pattern.ForwardSliceSearcher s) Id (String.Slice.Pattern.SearchStep s)
-- Mathlib.Data.Set.Prod
Set.diag_preimage_prod : ∀ {α : Type u_1} (s t : Set α), Function.diag ⁻¹' s ×ˢ t = s ∩ t
-- Init.Data.List.Perm
List.Sublist.exists_perm_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∃ l, l₂.Perm (l₁ ++ l)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The inverse image of a property of objects by a functor.  -/
CategoryTheory.ObjectProperty.inverseImage : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.ObjectProperty D → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty C
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- The relative perfect closure of `F` in `E`, consists of the elements `x` of `E` such that there
exists a natural number `n` such that `x ^ (ringExpChar F) ^ n` is contained in `F`, where
`ringExpChar F` is the exponential characteristic of `F`. It is also the maximal purely inseparable
subextension of `E / F` (`le_perfectClosure_iff`).  -/
perfectClosure : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E
-- Lean.Elab.PreDefinition.PartialFixpoint.Main
Lean.Elab.partialFixpoint : Lean.LocalContext × Lean.LocalInstances → Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.Order.Sublattice
Sublattice.le_comap_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β)
  (L : ι → Sublattice β), ⨆ i, Sublattice.comap f (L i) ≤ Sublattice.comap f (⨆ i, L i)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl_zero : ∀ (α : Type u_1) (V : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq α] [inst_3 : DecidableEq V],
  Matrix.compl 0 = SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V)
-- Init.Sym.Simp.SimprocDSL
/-- Identity simproc (no simplification).  -/
Lean.Parser.Sym.Simp.none : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Finprod
single_le_finprod : ∀ {α : Type u_1} {M : Type u_7} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] (i : α) {f : α → M},
  Function.HasFiniteMulSupport f → (∀ (j : α), 1 ≤ f j) → f i ≤ ∏ᶠ (j : α), f j
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.match_1.eq_2 : ∀ {α : Type u_2} (motive : (x : ℕ) → ((i : ℕ) → i < x → α → α) → α → Sort u_1) (n : ℕ)
  (f : (i : ℕ) → i < n.succ → α → α) (a : α) (h_1 : (f : (i : ℕ) → i < 0 → α → α) → (a : α) → motive 0 f a)
  (h_2 : (n : ℕ) → (f : (i : ℕ) → i < n.succ → α → α) → (a : α) → motive n.succ f a),
  (match n.succ, f, a with
    | 0, f, a => h_1 f a
    | n.succ, f, a => h_2 n f a) =
    h_2 n f a
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)),
  (CategoryTheory.Over.ConstructProducts.conesEquiv B F).unitIso =
    CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence pairwise preserves non-negative distance. Forward direction of
`congruent_iff_pairwise_nndist_eq`.  -/
Congruent.pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Congruent v₁ v₂ → Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.Equiv t₂ → t₁.maxKey! = t₂.maxKey!
-- Mathlib.Data.Matrix.Basic
/-- The `AddMonoidHom` between spaces of matrices induced by an `AddMonoidHom` between their
coefficients. This is `Matrix.map` as an `AddMonoidHom`.  -/
AddMonoidHom.mapMatrix : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_11} →
      {β : Type u_12} → [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) → Matrix m n α →+ Matrix m n β
-- Mathlib.Order.SetNotation
Set.sSup_eq_sUnion : ∀ {α : Type u} (S : Set (Set α)), sSup S = ⋃₀ S
-- Mathlib.Algebra.BigOperators.Ring.Finset
Commute.sum_right : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Finset ι) (f : ι → R) (b : R),
  (∀ i ∈ s, Commute b (f i)) → Commute b (∑ i ∈ s, f i)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map.eq_1 : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F']
  (f : F ⟶ F'),
  CategoryTheory.Limits.end_.map f =
    CategoryTheory.Limits.end_.lift
      (fun x => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F x) ((f.app (Opposite.op x)).app x)) ⋯
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_slice : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, (s.slice p₁ p₂ h).isEmpty = true ↔ p₁ = p₂
-- Std.Do.SPred.DerivedLaws
/-- A proof that the original stateful predicate is equivalent to the decomposed form.
 -/
Std.Do.SPred.Tactic.HasFrame.reassoc : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {P' : outParam (Std.Do.SPred σs)} {φ : outParam Prop}
  [self : Std.Do.SPred.Tactic.HasFrame P P' φ], P ⊣⊢ₛ P' ∧ ⌜φ⌝
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_self_left : ∀ {m n : ℕ}, (m + n).Coprime n ↔ m.Coprime n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, t.contains a = true)
-- Mathlib.Analysis.Convex.Basic
Convex.setOfPred_const_imp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {P : Prop}, Convex 𝕜 s → Convex 𝕜 {x | P → x ∈ s}
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_minKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {kme : α},
      Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = some kme → Std.Internal.List.containsKey kme l = true
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying binary relation.  -/
Con.coe_sInf : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), ⇑(sInf S) = sInf (DFunLike.coe '' S)
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.getAnchor.match_1.eq_2 : ∀ (motive : Option UInt64 → Sort u_1) (x : Option UInt64) (h_1 : (a : UInt64) → motive (some a))
  (h_2 : (x : Option UInt64) → motive x),
  (∀ (a : UInt64), x = some a → False) →
    (match x with
      | some a => h_1 a
      | x => h_2 x) =
      h_2 x
-- Init.Control.Lawful.MonadLift.Instances
OptionT.instLawfulMonadLift : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m], LawfulMonadLift m (OptionT m)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The object property on `Comma L R` induced by a morphism property.  -/
CategoryTheory.MorphismProperty.commaObj : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                CategoryTheory.MorphismProperty T → CategoryTheory.ObjectProperty (CategoryTheory.Comma L R)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally, then derivatives within these sets coincide locally.  -/
mfderivWithin_eventually_congr_set : ∀ {𝕜 : 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' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  s =ᶠ[nhds x] t → ∀ᶠ (y : M) in nhds x, mfderiv[s] f y = mfderiv[t] f y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_le_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  {a : A} (ha : p a) {f g : C(↑(spectrum R a), R)}, (cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app : ∀ {C : Type u_2} {D : Type u_3} {E : Type u_4} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory C] [inst_4 : CategoryTheory.CartesianMonoidalCategory E]
  (F G : CategoryTheory.Functor D C) (H : CategoryTheory.Functor C E)
  [inst_5 : CategoryTheory.Limits.PreservesFiniteProducts H] (X : D),
  (CategoryTheory.Functor.Monoidal.tensorObjComp F G H).inv.app X =
    (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso H (F.obj X) (G.obj X)).inv
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_mul : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) (a R : ℝ) (x : P),
  EuclideanGeometry.inversion c (a * R) x = (AffineMap.homothety c (a ^ 2)) (EuclideanGeometry.inversion c R x)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_prod_mk_eval₂ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R) (j : τ)
  (g : σ → MvPolynomial σ R),
  (MvPolynomial.rename (Prod.mk j)) (MvPolynomial.eval₂ MvPolynomial.C g p) =
    MvPolynomial.eval₂ MvPolynomial.C (fun x => (MvPolynomial.rename (Prod.mk j)) (g x)) p
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- For every set there exists a measurable superset of the same measure.  -/
MeasureTheory.exists_measurable_superset : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s
-- Mathlib.Data.Subtype
Subtype.refl : ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] (s : Subtype p), s ≈ s
-- Mathlib.ModelTheory.Encoding
/-- Decodes a list of symbols as a list of formulas.  -/
FirstOrder.Language.BoundedFormula.sigmaImp_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  FirstOrder.Language.BoundedFormula.sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ.imp ψ⟩
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_encode_lt_top : ∀ {r : ENNReal}, r < 1 → ∀ {ι : Type u_4} [inst : Encodable ι], ∑' (i : ι), r ^ Encodable.encode i < ⊤
-- Std.Http.Protocol.H1.Writer
/-- Writes accumulated user data to output as raw bytes (HTTP/1.0 connection-close framing).
No chunk framing is added; the peer reads until the connection closes.
 -/
Std.Http.Protocol.H1.Writer.writeRawBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.symm_toPartialEquiv : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.symm.toPartialEquiv = e.toPartialEquiv.symm
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A univariate polynomial `Q₂` that satisfies `Q₂ * Φ = θ`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₂ : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → Polynomial K
-- Mathlib.Analysis.Convex.Between
/-- If `T` is an affine independent family of points,
then any 3 distinct points form a triangle.  -/
AffineIndependent.not_wbtw_of_injective : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {ι : Type u_6} (i j k : ι),
  Function.Injective ![i, j, k] → ∀ {T : ι → P}, AffineIndependent R T → ¬Wbtw R (T i) (T j) (T k)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.units_smul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (k : Rˣ)
  (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  (k • z₁).comp z₂ h = k • z₁.comp z₂ h
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.min?.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c RBTree.RBNode.nil v r)) →
          ((c : RBTree.RBColor) →
              (l : RBTree.RBNode α) →
                (v : α) →
                  (r : RBTree.RBNode α) → (l = RBTree.RBNode.nil → False) → motive (RBTree.RBNode.node c l v r)) →
            motive x