mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.π.eq_1 : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M), solution.π = Finsupp.linearCombination A solution.var
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.isCycle_cycle : ∀ {n : ℕ}, (SimpleGraph.cycleGraph.cycle n).IsCycle
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.contDiff_cos : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.cos
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.eq : ℕ →
  Lean.Expr →
    Lean.Expr → Lean.Meta.Grind.PendingSolverPropagationsData✝ → Lean.Meta.Grind.PendingSolverPropagationsData✝
-- Mathlib.SetTheory.Lists
instDecidableEqLists' : {α : Type u_2} → {a : Bool} → [DecidableEq α] → DecidableEq (Lists' α a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A multiple of the difference between two points lies in their `vectorSpan`.  -/
smul_vsub_mem_vectorSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₁ -ᵥ p₂) ∈ vectorSpan k {p₁, p₂}
-- Mathlib.GroupTheory.Torsion
MulEquiv.comap_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] (e : G ≃* H),
  Subgroup.comap (↑e) (CommGroup.torsion H) = CommGroup.torsion G
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightId.congr_simp : ∀ {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) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso],
  CategoryTheory.MorphismProperty.Comma.mapRightId L R = CategoryTheory.MorphismProperty.Comma.mapRightId L R
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity scales distance. Forward direction of `similar_iff_exists_dist_eq`.  -/
Similar.exists_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isLittleO_deriv_one_sub_smoothingFn : (deriv fun x => 1 - AkraBazziRecurrence.smoothingFn x) =o[Filter.atTop] fun x => x⁻¹
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_pow_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s t : Finset α} {n : ℕ}, (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
-- Lean.Meta.Tactic.Simp.Types
/-- User-extensible configuration. Tactic options of the form `(user.optName := ...)`
set keys `tactic.simp.user.optName`, if there is a global option named `tactic.simp.user.optName`.  -/
Lean.Meta.Simp.Context.userConfig : Lean.Meta.Simp.Context → Lean.Options
-- Mathlib.Topology.MetricSpace.Contracting
/-- A map is said to be `ContractingWith K`, if `K < 1` and `f` is `LipschitzWith K`.  -/
ContractingWith : {α : Type u_1} → [EMetricSpace α] → NNReal → (α → α) → Prop
-- Mathlib.Combinatorics.Matroid.Basic
/-- `M` has a predicate `Base` defining its bases.  -/
Matroid.IsBase : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite symmetric
forms.  -/
LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M) [Module.IsTorsionFree R M],
  (∀ (x : M), x ≠ 0 → 0 < (B x) x) →
    LinearMap.IsSymm B → ∀ (x y : M), (B x) y ^ 2 < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.comp_continuousOn_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {α : Type u_11} [inst_8 : TopologicalSpace α] {f : α → E} {s : Set α},
  ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A Borel-measurable set in a Polish space is analytic.  -/
MeasurableSet.analyticSet : ∀ {α : Type u_3} [t : TopologicalSpace α] [PolishSpace α] [inst : MeasurableSpace α] [BorelSpace α] {s : Set α},
  MeasurableSet s → MeasureTheory.AnalyticSet s
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- Summing `a^#s * b^(n-#s)` over all finite subsets `s` of a fintype of cardinality `n`
gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that
`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead
a proof reducing to the usual binomial theorem to have a result over semirings.  -/
Fintype.sum_pow_mul_eq_add_pow : ∀ {R : Type u_4} [inst : CommSemiring R] (ι : Type u_5) [inst_1 : Fintype ι] (a b : R),
  ∑ s, a ^ s.card * b ^ (Fintype.card ι - s.card) = (a + b) ^ Fintype.card ι
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsStarNormal.norm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsStarNormal a → IsStarNormal b → Commute a b → a * b = 0 → ‖a - b‖ = max ‖a‖ ‖b‖
-- Lean.Expr
Lean.Expr.updateLet! : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- A variant of `AffineBasis.affineCombination_coord_eq_self` for the special case when the
affine space is a module so we can talk about linear combinations.  -/
AffineBasis.linear_combination_coord_eq_self : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k] [inst_2 : Module k V]
  [inst_3 : Fintype ι] (b : AffineBasis ι k V) (v : V), ∑ i, (b.coord i) v • b i = v
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.instTypeNameRealizeConstantResult : TypeName Lean.Meta.RealizeConstantResult✝
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.next_f_of_not_boundaryLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {j k : ι}, c.next j = k → ¬e.BoundaryLE j → c'.next (e.f j) = e.f k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  m.WF →
    ((Std.DHashMap.Raw.filterMap f m).isEmpty = false ↔
      ∃ k, ∃ (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Raw.Const.get m k h)).isSome = true)
-- Mathlib.MeasureTheory.Measure.Regular
/-- The restriction of a weakly regular measure to a measurable set of finite measure is
weakly regular.  -/
MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [BorelSpace α]
  [μ.WeaklyRegular] {A : Set α}, μ A ≠ ⊤ → (μ.restrict A).WeaklyRegular
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_mul : ∀ {n : ℕ} (x y : ℤ), BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- `rTensor A f : B ⊗ A →ₐc C ⊗ A` is the natural bialgebra morphism induced by `f : B →ₐc C`.  -/
BialgHom.rTensor : {R : Type u_1} →
  (A : Type u_2) →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : Ring A] →
            [inst_2 : Ring B] →
              [inst_3 : Ring C] →
                [inst_4 : Bialgebra R A] →
                  [inst_5 : Bialgebra R B] →
                    [inst_6 : Bialgebra R C] → (B →ₐc[R] C) → TensorProduct R B A →ₐc[R] TensorProduct R C A
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_mul : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ * s = x • Metric.cthickening δ s
-- Lean.Meta.DiscrTree.Main
/-- whnf for the discrimination tree module  -/
Lean.Meta.DiscrTree.reduceDT : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- An object of the original category produces a formal coproduct on that object only, so indexed
by `PUnit`, the type with one element.  -/
CategoryTheory.Limits.FormalCoproduct.incl : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.Algebra.Group.End
Equiv.swap_apply_apply : ∀ {α : Type u_4} [inst : DecidableEq α] (f : Equiv.Perm α) (x y : α), Equiv.swap (f x) (f y) = f * Equiv.swap x y * f⁻¹
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_map_toDual`. -/
List.SortedGT.map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.toDual) l).SortedGT → l.SortedLT
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_symm_succ : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (Equiv.symm i.cycleRange) j.succ = i.succAbove j
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomHomAssociator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y] [inst_5 : CategoryTheory.MonObj Z],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.Data.Set.Image
sigma_mk_preimage_image' : ∀ {α : Type u_1} {β : α → Type u_2} {i j : α} {s : Set (β i)}, i ≠ j → Sigma.mk j ⁻¹' Sigma.mk i '' s = ∅
-- Mathlib.GroupTheory.CosetCover
Subgroup.leftCoset_cover_filter_FiniteIndex_aux : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred Subgroup.FiniteIndex],
      ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
        1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
          (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i • ↑(H i))
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_of_mem : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α]
  (h : a ∈ lowerClosure ↑s), s.truncatedSup a = {b ∈ s | a ≤ b}.sup' ⋯ id
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.decidablePred : {α : Type u_1} → [inst : Compl α] → [DecidableEq α] → DecidablePred Heyting.IsRegular
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, (Std.HashSet.emptyWithCapacity c).get? a = none
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, then `S'.a` and `S'.b` are both congruent to `1` modulo `λ ^ 4` or are
both congruent to `-1`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ 4 ∣ FermatLastTheoremForThreeGen.Solution'.a✝ S' ^ 3 - 1 ∧
      (hζ.toInteger - 1) ^ 4 ∣ FermatLastTheoremForThreeGen.Solution'.b✝ S' ^ 3 + 1 ∨
    (hζ.toInteger - 1) ^ 4 ∣ FermatLastTheoremForThreeGen.Solution'.a✝ S' ^ 3 + 1 ∧
      (hζ.toInteger - 1) ^ 4 ∣ FermatLastTheoremForThreeGen.Solution'.b✝ S' ^ 3 - 1
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mul_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  (x : R), ‖(ContinuousLinearMap.mul 𝕜 R) x‖ = ‖x‖
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_pos : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], 0 < G.degree v ↔ ¬G.IsIsolated v
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g') h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) h_1)
-- Mathlib.CategoryTheory.Sites.Closed
/-- Any sieve is smaller than its closure.  -/
CategoryTheory.GrothendieckTopology.le_close : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X), S ≤ J₁.close S
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `s ×ˢ t` is homeomorphic to `s × t`.  -/
Homeomorph.Set.prod : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (s : Set X) → (t : Set Y) → ↑(s ×ˢ t) ≃ₜ ↑s × ↑t
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.ext : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (h_X : C₁.X = C₂.X),
  (∀ (i j : ι),
      c.Rel i j →
        CategoryTheory.CategoryStruct.comp (C₁.d i j) (CategoryTheory.eqToHom ⋯) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C₂.d i j)) →
    C₁ = C₂
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_div : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x y : R), WithVal.toVal v (x / y) = WithVal.toVal v x / WithVal.toVal v y
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq : ∀ (n : ℕ), (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The shadow of the empty set is empty.  -/
Finset.shadow_empty : ∀ {α : Type u_1} [inst : DecidableEq α], ∅.shadow = ∅
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAddEquiv_refl_refl : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : Add R],
  Matrix.reindexAddEquiv R (Equiv.refl m) (Equiv.refl n) = AddEquiv.refl (Matrix m n R)
-- Mathlib.MeasureTheory.Measure.Support
/-- If the complement of the support is Lindelöf, then the support of a measure is conull.  -/
MeasureTheory.Measure.support_mem_ae_of_isLindelof : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  IsLindelof μ.supportᶜ → μ.support ∈ MeasureTheory.ae μ
-- Mathlib.CategoryTheory.Monad.Types
/-- **Alias** of `CategoryTheory.kleisliCatEquivKleisli`.

---

The `Kleisli` category of a `Control.Monad` is equivalent to the `Kleisli` category of its
category-theoretic version, provided the monad is lawful.
 -/
CategoryTheory.eq : (m : Type u → Type u) →
  [inst : Monad m] →
    [inst_1 : LawfulMonad m] → CategoryTheory.KleisliCat m ≌ CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.functorCategoryEquivalenceFunctorMonoidal : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] → (Action.functorCategoryEquivalence V G).functor.Monoidal
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.monoModSerre.isoModSerre_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsSerreClass] {X Y : C} {f : X ⟶ Y},
  P.monoModSerre f → P.isoModSerre (CategoryTheory.Abelian.factorThruImage f)
-- Std.Data.ExtDTreeMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.ExtDTreeMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.productiveRel_of_right₁ : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ it₂' : Std.IterM m β},
  InvImage Std.IterM.TerminationMeasures.Productive.Rel Std.IterM.finitelyManySkips it₂' it₂ →
    Std.Iterators.Types.Flatten.ProductiveRel✝ α β m { internalState := { it₁ := it₁, it₂ := some it₂' } }
      { internalState := { it₁ := it₁, it₂ := some it₂ } }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.isPullback₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁
-- Init.Classical
Classical.inhabited_of_exists : {α : Sort u} → {p : α → Prop} → (∃ x, p x) → Inhabited α
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  (J : Type u') [inst_1 : CategoryTheory.Category.{v', u'} J],
  HasCardinalLT (CategoryTheory.Arrow J) κ → (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  J.plusMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.plusObj P)
-- Mathlib.Data.PFun
PFun.dom_prodLift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ),
  (f.prodLift g).Dom = {x | (f x).Dom ∧ (g x).Dom}
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry₂.injEq : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p q : Mathlib.Tactic.ITauto.Proof) (ak_1 : Mathlib.Tactic.ITauto.AndKind)
  (p_1 q_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.curry₂ ak p q = Mathlib.Tactic.ITauto.Proof.curry₂ ak_1 p_1 q_1) =
    (ak = ak_1 ∧ p = p_1 ∧ q = q_1)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_top : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], -⊤ = ⊤
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec2_eq : ∀ {α : Type u} {a₀ a₁ b₀ b₁ : α}, a₀ = b₀ → a₁ = b₁ → ![a₀, a₁] = ![b₀, b₁]
-- Init.Data.Option.Basic
Option.getDM_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Pure m] (y : m α), none.getDM y = y
-- Mathlib.Algebra.Order.Group.Abs
abs_eq : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  0 ≤ b → (|a| = b ↔ a = b ∨ a = -b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.LawfulEqOrd α] [Std.TransOrd α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {k : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? l = some k ↔
      Std.Internal.List.containsKey k l = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The inclusion of the quiver on `V` to the underlying quiver on `FreeGroupoid V`  -/
Quiver.FreeGroupoid.of : (V : Type u_1) → [inst : Quiver V] → V ⥤q Quiver.FreeGroupoid V
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.measurePreserving_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.MeasurePreserving Prod.snd (μ.prod ν) ν
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
any open set.  -/
MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] (K : Set G),
  IsCompact K → μ K ≠ 0 → μ.IsOpenPosMeasure
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.exists_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop}, (∃ x, C x) ↔ ∃ x, C ↑x
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_nonpos : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β}, (∀ i ∈ f.support, h₁ i (f i) ≤ 0) → f.sum h₁ ≤ 0
-- Aesop.Rule.Name
Aesop.instBEqDisplayRuleName.beq : Aesop.DisplayRuleName → Aesop.DisplayRuleName → Bool
-- Mathlib.Order.UpperLower.Principal
/-- Principal lower set. `Set.Iic` as a lower set. The smallest lower set containing a given
element.  -/
LowerSet.Iic : {α : Type u_1} → [inst : Preorder α] → α → LowerSet α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.DTreeMap.Raw.ofList l cmp).inner.isEmpty = l.isEmpty
-- Mathlib.Data.List.AList
AList.singleton_entries : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a), (AList.singleton a b).entries = [⟨a, b⟩]
-- Mathlib.Logic.Relation
Relation.TransGen.trans_induction_on : ∀ {α : Type u_1} {r : α → α → Prop} {motive : {a b : α} → Relation.TransGen r a b → Prop} {a b : α}
  (h : Relation.TransGen r a b),
  (∀ {a b : α} (h : r a b), motive ⋯) →
    (∀ {a b c : α} (h₁ : Relation.TransGen r a b) (h₂ : Relation.TransGen r b c), motive h₁ → motive h₂ → motive ⋯) →
      motive h
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight (HomotopicalAlgebra.RightHomotopyClass.mk f) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.BifibrantObject.homMk f)