mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (ll lr : Std.DTreeMap.Internal.Impl α β) →
        ((lls : ℕ) →
            (k : α) →
              (v : β k) →
                (l r : Std.DTreeMap.Internal.Impl α β) →
                  (lrs : ℕ) →
                    (lrk : α) →
                      (lrv : β lrk) →
                        (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                          motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf) →
            ((x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x) → motive ll lr
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_sdiff_singleton : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {y : E}, ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.Analysis.Meromorphic.Order
/-- Meromorphic functions on `U` are analytic on `U`, outside of a discrete subset.  -/
MeromorphicOn.analyticAt_mem_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → {x | AnalyticAt 𝕜 f x} ∈ Filter.codiscreteWithin U
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_of_iso : ∀ {X Y : SSet} (e : X ≅ Y) [X.Finite], Y.Finite
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyLE.countable_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋂ i, s i ≤ᶠ[l] ⋂ i, t i
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_eq_div : ∀ {δ : Type u_4} [inst : CommGroup δ] (f : ℕ → δ) {m n : ℕ},
  m ≤ n → ∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) / ∏ k ∈ Finset.range m, f k
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.orElse.match_1.splitter : {α : Type u_1} →
  (motive : Option α → (Unit → Option α) → Sort u_2) →
    (x : Option α) →
      (x_1 : Unit → Option α) →
        ((a : α) → (x : Unit → Option α) → motive (some a) x) → ((b : Unit → Option α) → motive none b) → motive x x_1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_sup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  {S T : IntermediateField F E}, S.FG → T.FG → (S ⊔ T).FG
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_eq_mul_nodal_erase : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι] {i : ι},
  i ∈ s → Lagrange.nodal s v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal (s.erase i) v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr_eq_2 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : x = Ordering.lt → motive Ordering.lt)
  (h_2 : x = Ordering.eq → motive Ordering.eq) (h_3 : x = Ordering.gt → motive Ordering.gt) (heq_1 : x = Ordering.eq),
  (match h : x with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) ≍
    h_2 heq_1
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_dvd₂ : ∀ {s : ℤ} (a c d p x : ℤ), p ≤ a * x → d ∣ c * x + s → a * d ∣ c * Int.Cooper.resolve_left a c d p x + c * p + a * s
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_iff_integrable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : MeasureTheory.SimpleFunc α E},
  p ≠ 0 → p ≠ ⊤ → (MeasureTheory.MemLp (⇑f) p μ ↔ MeasureTheory.Integrable (⇑f) μ)
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, ∅.toList = []
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.inv_smul_integral_comp_add_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_injOn_pos : Set.InjOn Real.log (Set.Ioi 0)
-- Mathlib.Tactic.FunProp.Theorems
/-- Gives the theorem form using the result of `FunctionData.decomposition`.

Note that this returns `TheoremForm.comp` even when the decomposition failed (usually due to
dependent types). This means that the theorem will be applied directly without trying to write the
goal as a composition.  -/
Mathlib.Meta.FunProp.DecompositionResult.toTheoremForm : Mathlib.Meta.FunProp.DecompositionResult → Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.contDiffAt_rpow_const : ∀ {x p : ℝ} {n : ℕ}, x ≠ 0 ∨ ↑n ≤ p → ContDiffAt ℝ (↑n) (fun x => x ^ p) x
-- Std.Do.PostCond
Std.Do.PostCond.and_left_of_entails : ∀ {α : Type u_1} {ps : Std.Do.PostShape} {p q : Std.Do.PostCond α ps}, p.entails q → p = p.and q
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {q : ℚ},
  ↑q < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ↑q < a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.HashMap.Raw α β) (e_m : m = m_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.lift_unique : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C)
  (Φ : CategoryTheory.Functor (CategoryTheory.Paths V) C),
  CategoryTheory.Paths.of V ⋙q Φ.toPrefunctor = φ → Φ = CategoryTheory.Paths.lift φ
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multicospan index which shall be used
to define the end of `F`.  -/
CategoryTheory.Limits.multicospanIndexEnd : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) →
          CategoryTheory.Limits.MulticospanIndex (CategoryTheory.Limits.multicospanShapeEnd J) C
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, alternate form.

A module $M$ is flat if and only if for all finite free modules $R^l$,
all $f \in R^l$, and all linear maps $x \colon R^l \to M$ such that $x(f) = 0$, there
exist a finite free module $R^k$ and linear maps $a \colon R^l \to R^k$ and
$y \colon R^k \to M$ such that $x = y \circ a$ and $a(f) = 0$.  -/
Module.Flat.iff_forall_exists_factorization : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
CommCStarAlgebra.norm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCommCStarAlgebra A] {a b : A}, a * b = 0 → ‖a - b‖ = max ‖a‖ ‖b‖
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.Exact.exact_toComposableArrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.toComposableArrows.Exact
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s)
  {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).hom = t.fst
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_const_right : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x + C) l Filter.atTop
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_injective_iff₂ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂],
  Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.takeUntil : (Char → Bool) → Lean.ParseImports.Parser
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [inst_1 : E.HasPullbacks], E.toOneHypercover.toPreOneHypercover = E.toPreOneHypercover
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_dblXYZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblXYZ (⇑f ∘ P) = ⇑f ∘ (W'.baseChange A).dblXYZ P
-- Mathlib.RingTheory.TensorProduct.Pi
/-- Tensor product of rings commutes with finite products on the right.  -/
Algebra.TensorProduct.piRight : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra S A] →
                  [inst_6 : IsScalarTower R S A] →
                    {ι : Type u_4} →
                      (B : ι → Type u_5) →
                        [inst_7 : (i : ι) → Semiring (B i)] →
                          [inst_8 : (i : ι) → Algebra R (B i)] →
                            [Fintype ι] →
                              [DecidableEq ι] →
                                TensorProduct R A ((i : ι) → B i) ≃ₐ[S] (i : ι) → TensorProduct R A (B i)
-- Mathlib.Data.Finset.Card
Finset.one_lt_card_iff : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofNonUnitalStarAlgHom_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂) (a : A₁),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂) a = f a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Right.inv_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a : G₀}, 0 ≤ a⁻¹ ↔ 0 ≤ a
-- Init.Data.Fin.Lemmas
Fin.castSucc_castLE : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), (Fin.castLE h i).castSucc = Fin.castLE ⋯ i
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofChoiceInfo.inj : ∀ {i i_1 : Lean.Elab.ChoiceInfo}, Lean.Elab.Info.ofChoiceInfo i = Lean.Elab.Info.ofChoiceInfo i_1 → i = i_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.prec' : ∀ {n : ℕ} {f g : List.Vector ℕ n → ℕ} {h : List.Vector ℕ (n + 2) → ℕ},
  Nat.Primrec' f →
    Nat.Primrec' g → Nat.Primrec' h → Nat.Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
-- Mathlib.Topology.IsLocalHomeomorph
/-- A `OpenPartialHomeomorph` is a local homeomorphism on its source.  -/
IsLocalHomeomorphOn.OpenPartialHomeomorph.isLocalHomeomorphOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), IsLocalHomeomorphOn (↑e) e.source
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α], UniformContinuous fun x => -x
-- Init.Data.Array.Zip
/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`.  -/
Array.getElem?_zipWith' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : Array α} {l₂ : Array β} {f : α → β → γ} {i : ℕ},
  (Array.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_lhs_exact : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs₁ rhs₁ rhs₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
      Lean.Grind.AC.Seq.denote ctx rhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.Topology.Sets.Closeds
/-- Given `f : U → X` a continuous open embedding, the irreducible closeds of `U` are order isomorphic
to the irreducible closeds of `X` nontrivially intersecting the range of `f`.
 -/
TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : β → α) → Topology.IsOpenEmbedding f → TopologicalSpace.IrreducibleCloseds β ≃o ↑{V | (f ⁻¹' ↑V).Nonempty}
-- Mathlib.Data.ENat.Basic
ENat.add_lt_add_of_lt_of_le : ∀ {a b c d : ℕ∞}, c ≠ ⊤ → a < b → c ≤ d → a + c < b + d
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsArtinianScheme.isNoetherianScheme : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsArtinianScheme X], AlgebraicGeometry.IsNoetherian X
-- Mathlib.RingTheory.Polynomial.Basic
/-- If the coefficients of a polynomial belong to an ideal, then that ideal contains
the ideal spanned by the coefficients of the polynomial.  -/
span_le_of_C_coeff_mem : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)},
  (∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I) → Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)} ≤ I
-- Mathlib.NumberTheory.FLT.Basic
/-- Statement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial natural solution
when `n ≥ 3`.

This is now a theorem of Wiles and Taylor--Wiles; see
https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of
a proof.  -/
FermatLastTheorem : Prop
-- Lean.Setup
Lean.instReprModuleHeader : Repr Lean.ModuleHeader
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.pi_eval : ∀ {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) (a : A),
  (ContinuousMap.pi f) a = fun i => (f i) a
-- Mathlib.Data.List.Nodup
List.Nodup.pmap : ∀ {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a},
  (∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) → l.Nodup → (List.pmap f l H).Nodup
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_d4 : 3.1415 < Real.pi
-- Mathlib.Data.TypeVec
TypeVec.repeatEq.eq_def : ∀ (x : ℕ) (x_1 : TypeVec.{u_1} x),
  x_1.repeatEq =
    match x, x_1 with
    | 0, x => TypeVec.nilFun
    | n.succ, α => α.drop.repeatEq ::: Function.uncurry Eq
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Icc_pred_right_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  a ≤ b → insert b (Set.Icc a (Order.pred b)) = Set.Icc a b
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKeyD_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {fallback : α},
      (Std.Internal.List.maxKeyD (Std.Internal.List.Const.modifyKey k f l) fallback ==
          Std.Internal.List.maxKeyD l fallback) =
        true
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The induced topology on `M` from a family of continuous linear maps from `M`, which is the
coarsest topology that makes every map continuous.  -/
TopModuleCat.induced : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} → {I : Type u_1} → {X : I → TopModuleCat R} → ((i : I) → M ⟶ (X i).toModuleCat) → TopModuleCat R
-- Std.Data.HashSet.Lemmas
Std.HashSet.erase_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.erase a = ∅
-- Init.Control.Basic
/-- A `ForIn'` instance, which handles `for h : x in c do`,
can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.

Note that this instance will cause a potentially non-defeq duplication if both `ForIn` and `ForIn'`
instances are provided for the same type.
 -/
instForInOfForIn' : {m : Type u_1 → Type u_2} → {ρ : Type u_3} → {α : Type u_4} → {d : Membership α ρ} → [ForIn' m ρ α d] → ForIn m ρ α
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Auxiliary sequence of metric spaces, containing copies of `X 0`, ..., `X n`, where each
`X i` is glued to `X (i+1)` in an optimal way. The space at step `n+1` is obtained from the space
at step `n` by adding `X (n+1)`, glued in an optimal way to the `X n` already sitting there.  -/
GromovHausdorff.auxGluing : (X : ℕ → Type) →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    [∀ (n : ℕ), CompactSpace (X n)] → [∀ (n : ℕ), Nonempty (X n)] → (n : ℕ) → GromovHausdorff.AuxGluingStruct (X n)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCode : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Code a)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_apply : ∀ {α : Type u_1} {m : Set α → ENNReal} (s : Set α),
  (MeasureTheory.OuterMeasure.boundedBy m) s =
    ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M],
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) CategoryTheory.MonObj.one)
      CategoryTheory.MonObj.mul
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.isNontrivial_iff_nontrivial_units : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R],
  ValuativeRel.IsNontrivial R ↔ Nontrivial (ValuativeRel.ValueGroupWithZero R)ˣ
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.eq_1 : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (x : X) (s : Set X),
  Convexity.IsStarConvexSet R x s =
    ∀ ⦃y : X⦄,
      y ∈ s → ∀ ⦃a b : R⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), Convexity.convexCombPair a b ha hb hab x y ∈ s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.isOrtho_def : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {Q : QuadraticMap R M N} {x y : M},
  Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_expand_left : ∀ {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] {w x y z : P},
  Sbtw R w x y → Sbtw R x y z → Sbtw R w x z
-- Lean.Data.Array
/-- `maskArray mask xs` keeps those `x` where the corresponding entry in `mask` is `true`
 -/
Lean.Array.mask : {α : Type u_1} → Array Bool → Array α → Array α
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instPow : Pow ONote ONote
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_4 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match Lean.Grind.Linarith.Expr.zero with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_4 ()
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.congr_linearEquiv_apply_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommGroup W] [inst_4 : Module R W] (e : V ≃ₗ[R] W) (f : SpecialLinearGroup R V) (x : W),
  (fun x => ↑((SpecialLinearGroup.congr_linearEquiv e) f) x) x = e ((fun x => ↑f x) (e.symm x))
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A polynomial `Q₀` with coefficients in `K⟮X⟯` that satisfies `Q₀ * Φ = θ`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₀ : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial (RatFunc K)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Iio : ∀ {n : ℕ} (i : Fin n), Fin.val '' Set.Iio i = Set.Iio ↑i
-- Mathlib.Algebra.Ring.ULift
ULift.nonAssocRing : {R : Type u} → [NonAssocRing R] → NonAssocRing (ULift.{u_1, u} R)
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulRightLinearEquiv.congr_simp : ∀ (R : Type u_9) {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a a_1 : Aˣ), a = a_1 → Units.mulRightLinearEquiv R a = Units.mulRightLinearEquiv R a_1
-- Init.Data.SInt.Bitwise
Int64.or_neg_one : ∀ {a : Int64}, a ||| -1 = -1
-- Mathlib.RepresentationTheory.Basic
/-- Turns a `k`-module `A` with a compatible `DistribMulAction` of a monoid `G` into a
`k`-linear `G`-representation on `A`.  -/
Representation.ofDistribMulAction : (k : Type u_1) →
  (G : Type u_2) →
    (A : Type u_3) →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module k A] → [inst_4 : DistribMulAction G A] → [SMulCommClass G k A] → Representation k G A
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.star : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : TopologicalSpace R]
  [inst_1 : Star R] [ContinuousStar R] {f : α → R},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (star f) μ