mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The Hadamard determinant identity: `det A * star (det A) = (card n)^(card n)`.  -/
Matrix.IsHadamard.det_mul_star_det : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
-- Init.Data.List.Lemmas
List.nil_append_fun : ∀ {α : Type u_1}, (fun x => [] ++ x) = id
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [inst_1 : ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsMarkovKernel κ.condKernelReal
-- Aesop.Search.Expansion
Aesop.RuleResult.toEmoji : Aesop.RuleResult → String
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.div : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G},
  IsLUB s a → IsGLB t b → IsLUB (s / t) (a / b)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instMulAction.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.instMulAction = Function.Injective.mulAction SetLike.coe ⋯ ⋯
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_eventually_atBot : ∀ {β : Type u_4} {α : Type u_6} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {r : α → β → Prop},
  (∃ b, ∀ᶠ (a : α) in Filter.atBot, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atBot, ∃ b, ∀ a ≤ a₀, r a b
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_map_eq_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → ∀ (S : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'CompFst_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) (X : A), (F.prod'CompFst G).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.Rat.Lemmas
Rat.add_den_dvd : ∀ (q₁ q₂ : ℚ), (q₁ + q₂).den ∣ q₁.den * q₂.den
-- Mathlib.Data.Num.Lemmas
Num.add_one : ∀ (n : Num), n + 1 = n.succ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.get_eq_of_revSkipWhile_le_char : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos} (h₁ : pos' < pos), pos.revSkipWhile c ≤ pos' → pos'.get ⋯ = c
-- Mathlib.Topology.Constructions
Sum.discreteTopology : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : DiscreteTopology X]
  [hY : DiscreteTopology Y], DiscreteTopology (X ⊕ Y)
-- Init.Grind.Norm
Lean.Grind.not_eq_prop : ∀ (p q : Prop), (¬p = q) = (p = ¬q)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_right_mul_add : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {y * z + x, y} = Ideal.span {x, y}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_erase_le_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp ((t.erase k).maxKey he) (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.prop_iff_of_shortExact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {S : CategoryTheory.ShortComplex C},
  S.ShortExact → (P S.X₂ ↔ P S.X₁ ∧ P S.X₃)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ_id : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (h : optParam (p ≤ Submodule.comap LinearMap.id p) ⋯), p.mapQ p LinearMap.id h = LinearMap.id
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.noon.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.noon = 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup.append_left : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubAddAction.ofFixingAddSubgroup M s)) (i : Fin s.ncard),
  have Hs := ⋯;
  (SubAddAction.ofFixingAddSubgroup.append x) (Fin.castAdd n i) = ↑((Classical.choice Hs) i)
-- Mathlib.GroupTheory.Solvable
derivedSeries_antitone : ∀ (G : Type u_1) [inst : Group G], Antitone (derivedSeries G)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_filterMap_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  (Std.TreeMap.filterMap f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) t[k] = none
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.instCoeBacktrackConfig : Coe Lean.Meta.SolveByElim.SolveByElimConfig Lean.Meta.Tactic.Backtrack.BacktrackConfig
-- Mathlib.Data.Int.ModEq
Int.modEq_sub_modulus_iff : ∀ {n a b : ℤ}, a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.go.eq_2 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon.go k m (Lean.Grind.CommRing.Poly.add k_1 m_1 p_1) =
    Lean.Grind.CommRing.Poly.add (k * k_1) (m.mul m_1) (Lean.Grind.CommRing.Poly.mulMon.go k m p_1)
-- Mathlib.Topology.Order.LiminfLimsup
/-- An antitone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsSup` to the `Filter.liminf` of the image if the function is continuous at the `limsSup`
(and the filter is bounded from above and frequently bounded from below).  -/
Antitone.map_limsSup_of_continuousAt : ∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [OrderTopology S]
  {F : Filter R} [F.NeBot] {f : R → S},
  Antitone f →
    ContinuousAt f F.limsSup →
      autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) F) Antitone.map_limsSup_of_continuousAt._auto_1 →
        autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F) Antitone.map_limsSup_of_continuousAt._auto_3 →
          f F.limsSup = Filter.liminf f F
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.mul : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedCommRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt% p z p' → HasMFDerivAt% q z q' → HasMFDerivAt% (p * q) z (p z • q' + q z • p')
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α → Ordering) →
        (l : Std.DTreeMap.Internal.Impl α β) →
          (motive :
              (m : Std.DTreeMap.Internal.Impl α β) →
                (Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true) →
                  Sort u_3) →
            (m : Std.DTreeMap.Internal.Impl α β) →
              (hm : Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true) →
                ((hm :
                      Std.DTreeMap.Internal.Impl.contains' k l = true →
                        Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = true) →
                    motive Std.DTreeMap.Internal.Impl.leaf hm) →
                  ((size : ℕ) →
                      (k' : α) →
                        (v' : β k') →
                          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                            (hm :
                                Std.DTreeMap.Internal.Impl.contains' k l = true →
                                  Std.DTreeMap.Internal.Impl.contains' k
                                      (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) =
                                    true) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) hm) →
                    motive m hm
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences `R ≃L[R] R` are enumerated by `Rˣ`.  -/
ContinuousLinearEquiv.unitsEquivAut : (R : Type u_1) → [inst : Semiring R] → [inst_1 : TopologicalSpace R] → [ContinuousMul R] → Rˣ ≃ R ≃L[R] R
-- Mathlib.Data.List.Intervals
List.Ico.succ_top : ∀ {n m : ℕ}, n ≤ m → List.Ico n (m + 1) = List.Ico n m ++ [m]
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.QuasiFiniteAt.of_quasiFiniteAt_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal R) (q : Ideal S) [inst_4 : q.IsPrime] [inst_5 : p.IsPrime] [q.LiesOver p]
  (Q : Ideal (p.Fiber S)) [inst_7 : Q.IsPrime],
  Ideal.comap Algebra.TensorProduct.includeRight.toRingHom Q = q →
    ∀ [Algebra.QuasiFiniteAt p.ResidueField Q], Algebra.QuasiFiniteAt R q
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSemisimple.instBooleanAlgebra : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → [LieAlgebra.IsSemisimple R L] → BooleanAlgebra (LieIdeal R L)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.eq_of_succ_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] {a b : α}, Std.PRange.succ a = Std.PRange.succ b → a = b
-- Batteries.Data.List.Perm
List.Subperm.countP_le : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Subperm l₂ → List.countP p l₁ ≤ List.countP p l₂
-- Lean.Parser.Term
Lean.Parser.Term.letI.formatter : Lean.PrettyPrinter.Formatter
-- Lean.DocString.Markdown
/-- A way to transform inline elements extended with `i` into Markdown lines.
 -/
Lean.Doc.MarkdownInline : Type u → Type u
-- Mathlib.Data.Complex.Basic
Complex.im_nnqsmul : ∀ (q : ℚ≥0) (z : ℂ), (q • z).im = q • z.im
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.motive : Lean.Meta.RecursorUnivLevelPos
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.liftAddHom_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N] (f : M →+ N →+ P)
  (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) (m : M) (n : N),
  (TensorProduct.liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n
-- Mathlib.Algebra.Tropical.Basic
Tropical.zero_ne_trop_coe : ∀ {R : Type u} (x : R), 0 ≠ Tropical.trop ↑x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β k} {tl : List ((a : α) × β a)},
  ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany (⟨k, v⟩ :: tl)) =
    ↑((Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v).insertMany tl)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_nat : ∀ (n : ℕ), (↑n).card = ↑n
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The inverse of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.symm : {X Y : AlgebraicGeometry.Scheme} → X.PartialIso Y → Y.PartialIso X
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : ↥(unitary A)},
  ‖↑u - 1‖ < 2 → 2 * (1 - Real.cos ‖Unitary.argSelfAdjoint u‖) = ‖↑u - 1‖ ^ 2
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonGetWidgetSourceParams.fromJson : Lean.Json → Except String Lean.Widget.GetWidgetSourceParams
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.pos : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → it.i = { byteIdx := String.utf8Len l }
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.factorial_mul_dpow_eq_pow : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) {n : ℕ},
  a ∈ I → ↑n.factorial * hI.dpow n a = a ^ n
-- Mathlib.Data.Set.Image
Set.Nonempty.subset_preimage_const : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (t : Set β) (a : β), s ⊆ (fun x => a) ⁻¹' t ↔ a ∈ t
-- Init.Data.Range.Polymorphic.Map
Std.PRange.LawfulUpwardEnumerableLE.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LE α] [inst_3 : LE β] [Std.PRange.LawfulUpwardEnumerableLE β] (f : Std.PRange.UpwardEnumerable.Map α β)
  [f.PreservesLE], Std.PRange.LawfulUpwardEnumerableLE α
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Evaluation of the logarithmic counting function at zero yields zero.
 -/
Function.locallyFinsuppWithin.logCounting_eval_zero : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] (D : Function.locallyFinsupp E ℤ),
  Function.locallyFinsuppWithin.logCounting D 0 = 0
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_mulSingle : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop]
  {f : β → α} (b : β), (∀ (b' : β), b' ≠ b → f b' = 1) → ∏'[L] (b : β), f b = f b
-- Init.Data.UInt.Lemmas
USize.ofNat_toNat : ∀ {x : USize}, USize.ofNat x.toNat = x
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.MonCat.Hom.mk : {A B : MonCat} → (↑A →* ↑B) → A.Hom B
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.range_comp_val : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B),
  (f.comp S.val).range = Subalgebra.map f S
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) [P.RespectsIso] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  (P.inverseImage F).map F = P
-- Init.Data.List.MinMax
List.min_eq_head : ∀ {α : Type u} [inst : Min α] {l : List α} (hl : l ≠ []), List.Pairwise (fun a b => a ⊓ b = a) l → l.min hl = l.head hl
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.one_eq_mrange : ∀ {R : Type u_2} [inst : AddMonoidWithOne R], 1 = AddMonoidHom.mrange (Nat.castAddMonoidHom R)
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality. It is much cheaper than `isDefEq`.

This function is the main loop of `isDefEqS`
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqMain : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.measure_nullSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν), μ h.nullSet = 0
-- Mathlib.Topology.Order.Completion
/-- Every linear order embeds continuously in a dense complete linear order.  -/
Order.exists_dense_continuous_completion : ∀ (α : Type u) [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α],
  ∃ β x, ∃ (_ : DenselyOrdered β), ∃ x_2, ∃ (_ : OrderTopology β), ∃ ι, Continuous ⇑ι
-- Mathlib.Data.List.Nodup
List.Pairwise.nodup : ∀ {α : Type u} {l : List α} {r : α → α → Prop} [Std.Irrefl r], List.Pairwise r l → l.Nodup
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh_eq_sinh_div_cosh : ∀ (x : ℝ), Real.tanh x = Real.sinh x / Real.cosh x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst_1 : Inhabited α] {k : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).getKey! k = if k ∈ t then k else default
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.prod_antidiagonal_succ' : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M},
  ∏ p ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f p =
    f (n + 1, 0) * ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f (p.1, p.2 + 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keys_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {f : α → Bool},
  (Std.DTreeMap.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Aesop.Frontend.Saturate
Aesop.Frontend.elabAdditionalForwardRules : Aesop.LocalRuleSet → Array (Lean.TSyntax `Aesop.Frontend.Parser.additionalRule) → Aesop.ElabM Aesop.LocalRuleSet
-- Lean.LocalContext
Lean.instInhabitedLocalContext : Inhabited Lean.LocalContext
-- Mathlib.Order.SymmDiff
bot_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a : α), symmDiff ⊥ a = a
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.coe_finsetSum : ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
  (g : α → Π₀ (i : ι), β i), ⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass : {F : Type u_3} →
  {R : Type u_4} →
    {S : Type u_5} →
      {A : Type u_6} →
        {B : Type u_7} →
          [inst : Monoid R] →
            [inst_1 : Monoid S] →
              {φ : R →* S} →
                [inst_2 : NonUnitalNonAssocSemiring A] →
                  [inst_3 : DistribMulAction R A] →
                    [inst_4 : NonUnitalNonAssocSemiring B] →
                      [inst_5 : DistribMulAction S B] →
                        [inst_6 : FunLike F A B] → [NonUnitalAlgSemiHomClass F φ A B] → CoeTC F (A →ₛₙₐ[φ] B)
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instLTOrdinal : LT Std.Time.Week.OfYear.Ordinal
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] {Y' : C} (f f' : X ⟶ Y') (s : Y ⟶ Y')
  (hs : W s),
  sizeOf { Y' := Y', f := f, f' := f', s := s, hs := hs } = 1 + sizeOf Y' + sizeOf f + sizeOf f' + sizeOf s + sizeOf hs
-- Mathlib.Topology.VectorBundle.Basic
/-- The standard local trivializations of a vector bundle constructed from core are linear.  -/
VectorBundleCore.localTriv.isLinear : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι),
  Bundle.Trivialization.IsLinear R (Z.localTriv i)
-- Init.WFExtrinsicFix
/-- A fixpoint combinator that allows for deferred proofs of termination.

`extrinsicFix₂ R F` is function implemented as the loop
`extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b')`.

If the loop can be shown to be well-founded, `extrinsicFix₂_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, `extrinsicFix₂ R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
WellFounded.extrinsicFix₂ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {C₂ : (a : α) → β a → Sort u_3} →
      [∀ (a : α) (b : β a), Nonempty (C₂ a b)] →
        (R : (a : α) ×' β a → (a : α) ×' β a → Prop) →
          ((a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) →
            (a : α) → (b : β a) → C₂ a b
-- Std.Data.ExtTreeSet.Basic
/-- Folds the given function over the elements of the tree set in ascending order.  -/
Std.ExtTreeSet.foldl : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → [Std.TransCmp cmp] → (δ → α → δ) → δ → Std.ExtTreeSet α cmp → δ
-- Mathlib.Data.Multiset.AddSub
Multiset.card_erase_le : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, (s.erase a).card ≤ s.card
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `-i` and then shifting by `i` is the identity.  -/
CategoryTheory.shiftNegShift : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddGroup A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (X : C) → (i : A) → (CategoryTheory.shiftFunctor C i).obj ((CategoryTheory.shiftFunctor C (-i)).obj X) ≅ X
-- Mathlib.LinearAlgebra.Basis.Fin
/-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N`
and `y` and `N` together span the whole of `M`, then there is a basis for `M`
whose basis vectors are given by `Fin.cons y b`.  -/
Module.Basis.mkFinCons : {R : Type u_3} →
  {M : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {n : ℕ} →
            {N : Submodule R M} →
              (y : M) →
                Module.Basis (Fin n) R ↥N →
                  (∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) →
                    (∀ (z : M), ∃ c, z + c • y ∈ N) → Module.Basis (Fin (n + 1)) R M
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_congr : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, (φ₁ ↔ φ₂) → ⌜φ₁⌝ ⊣⊢ₛ ⌜φ₂⌝
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.add : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ ψ : MvPolynomial σ R},
  φ.IsSymmetric → ψ.IsSymmetric → (φ + ψ).IsSymmetric
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.GrothendieckTopology.HasSheafCompose.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor A B},
  (∀ (P : CategoryTheory.Functor Cᵒᵖ A),
      CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)) →
    J.HasSheafCompose F
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_right_inverse' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ᶠ (y : Y) in nhds (↑e x), ↑e (↑e.symm y) = y
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
/-- The cofibrations for the Quillen model category structure (TODO)
on `SSet` are monomorphisms.  -/
SSet.modelCategoryQuillen.instCategoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations SSet
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the horizontal composition `η ◫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.horizontalCompM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso