mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₁ → Std.DTreeMap.Const.getD (t₁ \ t₂) k fallback = fallback
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mk.congr_simp : ∀ {α : Type u_1} [inst : LE α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (upper' : IsUpperSet carrier), { carrier := carrier, upper' := upper' } = { carrier := carrier_1, upper' := ⋯ }
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.mem_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] {s : Set M} {y : N},
  y ∈ ProperCone.dual p s ↔ ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.op_vadd_set_stabilizer_subset : ∀ {G : Type u_1} [inst : AddGroup G] {a : G} {s : Set G}, a ∈ s → AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.var.inj : ∀ {i i_1 : Lean.Grind.Linarith.Var}, Lean.Grind.Linarith.Expr.var i = Lean.Grind.Linarith.Expr.var i_1 → i = i_1
-- Mathlib.CategoryTheory.Shift.Basic
/-- When `k = i + j`, shifting by `k` is the same as shifting by `i` and then shifting by `j`.  -/
CategoryTheory.shiftFunctorAdd' : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (i j k : A) →
            i + j = k →
              (CategoryTheory.shiftFunctor C k ≅
                (CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j))
-- Mathlib.Algebra.Category.ModuleCat.Free
ModuleCat.free_shortExact_finrank_add : ∀ {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact →
    ∀ {n p : ℕ} [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] [Module.Finite R ↑S.X₁] [Module.Finite R ↑S.X₃],
      Module.finrank R ↑S.X₁ = n →
        Module.finrank R ↑S.X₃ = p → ∀ [StrongRankCondition R], Module.finrank R ↑S.X₂ = n + p
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_add_le : ∀ {M : Type u_2} [inst : Add M] {s t : Set M} [IsCancelAdd M], Nat.card ↑(s + t) ≤ Nat.card ↑s * Nat.card ↑t
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.data : Lean.Meta.Grind.PendingSolverPropagations → Lean.Meta.Grind.PendingSolverPropagationsData✝
-- Batteries.Data.List.Lemmas
List.getElem_idxOfNth_beq : ∀ {α : Type u_1} {x : α} {n : ℕ} {xs : List α} [inst : BEq α] {h : List.idxOfNth x xs n < xs.length},
  (xs[List.idxOfNth x xs n] == x) = true
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_ric : ∀ {n i fallback : ℕ}, (*...=n).toList.getD i fallback = if i ≤ n then i else fallback
-- Init.Data.Float.Model.Unpacked.Basic
/-- Signed zero.  -/
Float.Model.UnpackedFloat.zero : Float.Model.UnpackedFloat.Sign → Float.Model.UnpackedFloat
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.Modules.toPresheaf X).Faithful
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_mul_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : CommSemigroup α] (a b : α), min a b * max a b = a * b
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.coeffIntegerNormalization_of_coeff_zero : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S) (i : ℕ),
  p.coeff i = 0 → IsLocalization.coeffIntegerNormalization M p i = 0
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `M` and `M'` are free (and lie in the same universe), the rank of `M × M'` is
`(Module.rank R M) + (Module.rank R M')`.  -/
rank_prod' : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M] [inst_4 : Module R M₁] [StrongRankCondition R] [Module.Free R M] [Module.Free R M₁],
  Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁
-- Mathlib.Algebra.Lie.Weights.Basic
/-- The set of weights is equivalent to a subtype.  -/
LieModule.Weight.equivSetOfPred : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] → LieModule.Weight R L M ≃ ↑{χ | LieModule.genWeightSpace M χ ≠ ⊥}
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_iff : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ ψ : L.Sentence},
  M ⊨ FirstOrder.Language.Formula.iff φ ψ ↔ (M ⊨ φ ↔ M ⊨ ψ)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommSemiRingCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommSemiRingCat)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instCommShiftCochainComplexIntQ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory.Q.CommShift ℤ
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_le_realToRCLike_iff : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] {f g : C(X, ℝ)},
  ContinuousMap.realToRCLike 𝕜 f ≤ ContinuousMap.realToRCLike 𝕜 g ↔ f ≤ g
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.mulEquivToLimit.congr_simp : ∀ (k : Type u_3) (K : Type u_4) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K],
  InfiniteGalois.mulEquivToLimit k K = InfiniteGalois.mulEquivToLimit k K
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.modify' : (Lean.Meta.Grind.Arith.Cutsat.State → Lean.Meta.Grind.Arith.Cutsat.State) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Interval.Basic
NonemptyInterval.dual_pure : ∀ {α : Type u_1} [inst : Preorder α] (a : α),
  NonemptyInterval.dual (NonemptyInterval.pure a) = NonemptyInterval.pure (OrderDual.toDual a)
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.instFaithfulHomotopyCategoryMapHomotopyCategoryOfFull : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Full] [F.Faithful] [inst_6 : F.Additive],
  (F.mapHomotopyCategory c).Faithful
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommMonoid : {M : Type u_3} → {N : Type u_4} → [AddCommMonoid M] → [AddCommMonoid N] → AddCommMonoid (M × N)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqSignature.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → Lean.Compiler.LCNF.Signature pu → Bool
-- Mathlib.NumberTheory.Height.NumberField
/-- A number field `K` satisfies the **Northcott property**:
The set of elements of bounded multiplicative height is finite.  -/
NumberField.finite_setOfPred_mulHeight₁_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ), {x | Height.mulHeight₁ x ≤ B}.Finite
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_union_iff : ∀ {α : Type v} {s t : Set α} [inst : LinearOrder α] [WellFoundedLT α],
  Order.cof α ≠ Cardinal.aleph0 → (IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_arrows_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B),
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (Opposite.op (X i))),
      CategoryTheory.Presieve.Arrows.Compatible P π x →
        ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If for any finitely generated submodules `M'` and `N'` of `M` and `N`, respectively,
`M'` and `N'` are linearly disjoint, then `M` and `N` themselves are linearly disjoint.  -/
Submodule.LinearDisjoint.of_linearDisjoint_fg : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (∀ (M' N' : Submodule R S), M' ≤ M → N' ≤ N → M'.FG → N'.FG → M'.LinearDisjoint N') → M.LinearDisjoint N
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 x_4 : x ⟶ x_1) (Γ : x_3 ⟶ x_4) (η : x_1 ⟶ x_2) (a : B),
  (CategoryTheory.Bicategory.whiskerRight Γ η).as.app a = CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (η.app a)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff.injEq : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] (coeff coeff_1 : M →₀ R),
  (AddMonoidAlgebra.ofCoeff coeff = AddMonoidAlgebra.ofCoeff coeff_1) = (coeff = coeff_1)
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.mk_smul : ∀ {α : Type u_1} {f : α → α} (n : ℕ) (x : α), { val := n } • x = f^[n] x
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instLieRing : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → LieRing (LeftInvariantDerivation I G)
-- Mathlib.Topology.Inseparable
SeparationQuotient.instSubsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Subsingleton X], Subsingleton (SeparationQuotient X)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1-cocycles `Z¹(G, A)` of `A : Rep k G`, defined as the kernel of the map
`Fun(G, A) → Fun(G × G, A)` sending `(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).`  -/
groupCohomology.cocycles₁ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u_1, u, u} k G) → Submodule k (G → ↑A)
-- Mathlib.Order.Fin.Finset
Fin.orderIsoSingleton_apply : ∀ {α : Type u_1} [inst : Preorder α] (a : α) (i : Fin 1), ↑((Fin.orderIsoSingleton a) i) = a
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.coindep_iff_compl_spanning : ∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.coindep_iff_compl_spanning._auto_1 → (M.Coindep I ↔ M.Spanning (M.E \ I))
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- A continuous linear map admits a right inverse which is a continuous linear map itself.  -/
ContinuousLinearMap.HasRightInverse : {R : Type u_1} →
  [inst : Semiring R] →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace F] → [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → (E →L[R] F) → Prop
-- Mathlib.Order.Defs.Unbundled
Std.Total.to_refl : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Refl r
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.projₗ_apply : ∀ (p : ENNReal) {𝕜 : Type u_1} {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)] (i : ι) (x : PiLp p β),
  (PiLp.projₗ p β i) x = x.ofLp i
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_natCast : ∀ {r : ℝ} {n : ℕ}, n ≠ 0 → (r.toNNReal = ↑n ↔ r = ↑n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keysArray.back?.getD fallback
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
MeasureTheory.StronglyMeasurable.limUnder : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace E] [Countable ι]
  {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [hE : Nonempty E]
  [TopologicalSpace.IsCompletelyMetrizableSpace E],
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
    MeasureTheory.StronglyMeasurable fun x => l.limUnder fun x_1 => f x_1 x
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Comp.mk.inj : ∀ {str : Mathlib.Ineq} {coeffs : Mathlib.Tactic.Linarith.Linexp} {str_1 : Mathlib.Ineq}
  {coeffs_1 : Mathlib.Tactic.Linarith.Linexp},
  { str := str, coeffs := coeffs } = { str := str_1, coeffs := coeffs_1 } → str = str_1 ∧ coeffs = coeffs_1
-- Mathlib.Data.List.Sublists
List.nodup_sublists' : ∀ {α : Type u} {l : List α}, l.sublists'.Nodup ↔ l.Nodup
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.mono_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V₁ V₂ : Submodule 𝕜 E}, V₂ ≤ V₁ → U ⟂ V₁ → U ⟂ V₂
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.propertyIsLocal : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Init.Grind.ToInt
Lean.Grind.IntInterval.io.inj : ∀ {hi hi_1 : ℤ}, Lean.Grind.IntInterval.io hi = Lean.Grind.IntInterval.io hi_1 → hi = hi_1
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instAlgebra : {R : Type u_3} →
  {A : Type u_4} →
    {M : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R M] → [inst_5 : Module A M] → [IsScalarTower R A M] → Algebra R (TensorAlgebra A M)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_reflect : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) (k : ℕ) {m n : ℕ},
  m ≤ n + 1 → ∏ j ∈ Finset.Ico k m, f (n - j) = ∏ j ∈ Finset.Ico (n + 1 - m) (n + 1 - k), f j
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instSemilatticeInf.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf GroupTopology.toTopologicalSpace ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (S : Subsemigroup N),
  Subsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯ }
-- Mathlib.Algebra.CharP.Basic
MulOpposite.charP : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p], CharP Rᵐᵒᵖ p
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionContext : Lean.ToJson Lean.Lsp.CodeActionContext
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ AddCommGrpCat AddCommMonCat
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_pos : ∀ {n : ℕ}, 0 < Nat.fib n ↔ 0 < n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.find?_some : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {x : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut],
  RBTree.RBNode.Ordered cmp t → (RBTree.RBNode.find? cut t = some x ↔ x ∈ t ∧ cut x = Ordering.eq)
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.mk.inj : ∀ {moduleNameMap : Std.HashMap Lean.Name Lean.ImportedModule✝} {moduleNames : Array Lean.Name}
  {moduleNameMap_1 : Std.HashMap Lean.Name Lean.ImportedModule✝} {moduleNames_1 : Array Lean.Name},
  { moduleNameMap := moduleNameMap, moduleNames := moduleNames } =
      { moduleNameMap := moduleNameMap_1, moduleNames := moduleNames_1 } →
    moduleNameMap = moduleNameMap_1 ∧ moduleNames = moduleNames_1
-- Mathlib.Order.Monotone.Basic
monotone_int_of_le_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α}, (∀ (n : ℤ), f n ≤ f (n + 1)) → Monotone f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.map f m},
  (Std.HashMap.map f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.opcyclesFunctor C).map φ = CategoryTheory.ShortComplex.opcyclesMap φ
-- Mathlib.Data.PEquiv
PEquiv.symm_bijective : ∀ {α : Type u} {β : Type v}, Function.Bijective PEquiv.symm
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.instMembership : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Membership α (Aesop.OrderedHashSet α)
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.instFiniteSubtypePosNeEndPos : ∀ {m : Type → Type u_1} {s : String.Slice} [inst : Pure m], Std.Iterators.Finite s.RevPosIterator m
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of a subgroup `s` of a seminormed group `E`, its norm in `s` is equal to
its norm in `E`.  -/
SubgroupClass.coe_norm : ∀ {E : Type u_1} [inst : SeminormedGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : SubgroupClass S E] (s : S)
  (x : ↥s), ‖x‖ = ‖↑x‖
-- Mathlib.Analysis.Real.Sqrt
NNReal.le_sqrt_iff_sq_le : ∀ {x y : NNReal}, x ≤ NNReal.sqrt y ↔ x ^ 2 ≤ y
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fst_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (self : α × β), (OrderMonoidHom.fst α β) self = self.1
-- Init.Data.List.Lemmas
/-- Every list is either empty, a non-empty `replicate`, or begins with a non-empty `replicate`
followed by a different element.  -/
List.eq_replicate_or_eq_replicate_append_cons : ∀ {α : Type u_1} (l : List α),
  l = [] ∨ (∃ n a, l = List.replicate n a ∧ 0 < n) ∨ ∃ n a b l', l = List.replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The submodule spanning the differences of a (possibly empty) set of points.  -/
vectorSpan : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] → [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [AddTorsor V P] → Set P → Submodule k V
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.ofBaseChange_comp_toBaseChange : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V),
  (CliffordAlgebra.ofBaseChange A Q).comp (CliffordAlgebra.toBaseChange A Q) =
    AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))
-- Mathlib.Data.List.Sort
List.SortedLE.sortedLT_of_nodup : ∀ {α : Type u_1} [inst : PartialOrder α] {l : List α}, l.SortedLE → l.Nodup → l.SortedLT
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaFiberFromRel_symm_apply_coe : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {f : α → β} (hf : r ≤ ⇑(Setoid.ker f))
  (z : (b : β) × ↑(Sym2.fromRel ⋯)), ↑((Equiv.sigmaFiberFromRel sym hf).symm z) = Sym2.map Subtype.val ↑z.snd
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasHomology]
  [inst_6 : (S.map F).HasHomology] [inst_7 : F.PreservesLeftHomologyOf S], S.mapHomologyIso F = S.mapHomologyIso F
-- Mathlib.Algebra.Opposites
MulOpposite.instSubsingleton : ∀ {α : Type u_1} [Subsingleton α], Subsingleton αᵐᵒᵖ
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n : ℕ),
  newton_seq_aux✝ hnorm n = newton_seq_aux✝ hnorm n
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_insert_le : ∀ {α : Type u_1} [inst : EDist α] {x : α} {s : Set α}, (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A simplified version of `IsRegular.recIterModByRegularWithRing` where the
motive is not allowed to depend on the proof of `IsRegular`.  -/
RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRing : {motive :
    (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} →
  ((R : Type u) →
      [inst : CommRing R] →
        (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Nontrivial M] → motive R M []) →
    ({R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    IsSMulRegular M r →
                      RingTheory.Sequence.IsRegular (QuotSMulTop r M)
                          (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
                        motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
                            (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
                          motive R M (r :: rs)) →
      {R : Type u} →
        [inst : CommRing R] →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → RingTheory.Sequence.IsRegular M rs → motive R M rs
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_sdiff_lt_prod_sdiff : ∀ {ι : Type u_9} {M : Type u_10} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M]
  [inst_3 : DecidableEq ι] {s t : Finset ι} {f : ι → M},
  ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
-- Init.Data.Range.Lemmas
/-- Generalization of `mem_of_mem_range'` used in `forIn'_loop_eq_forIn'_range'` below.  -/
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.mem_of_mem_range'_aux : ∀ {i : ℕ} {r : Std.Legacy.Range} {a : ℕ},
  (i - r.start) % r.step = 0 → r.start ≤ i → a ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step → a ∈ r
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_symm_apply_val : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2))
  (s : Subtype (CategoryTheory.Presieve.Arrows.Compatible F E.f)) (i : E.I₀),
  ((E.sectionsEquivOfHasPullbacks F).symm s).val i = ↑s i
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.Γ_map_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y),
  AlgebraicGeometry.SheafedSpace.Γ.map f.op = f.hom.c.app (Opposite.op ⊤)