mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ} {x : E},
  0 < D → x ∉ Metric.ball 0 (1 + D) → ExistsContDiffBumpBase.y D x = 0
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- Isometric equivalences are isometric maps  -/
QuadraticMap.IsometryEquiv.toIsometry : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → Q₁.IsometryEquiv Q₂ → Q₁ →qᵢ Q₂
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.reindexₗ.eq_1 : ∀ {m : Type u_1} {n : Type u_2} (R : Type u_3) (A : Type u_5) {l : Type u_7} {o : Type u_8} [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ l) (eₙ : n ≃ o),
  CStarMatrix.reindexₗ R A eₘ eₙ =
    { toFun := (Matrix.reindex eₘ eₙ).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Matrix.reindex eₘ eₙ).invFun,
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_true_iff_exists_contains_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool},
  m.WF → (m.any p = true ↔ ∃ a, ∃ (h : m.contains a = true), p a (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_trans_self : ∀ {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₂), e.symm.trans e = LinearIsometryEquiv.refl R₂ E₂
-- Mathlib.GroupTheory.Complement
Subgroup.not_isComplement_empty_right : ∀ {G : Type u_1} [inst : Group G] {S : Set G}, ¬Subgroup.IsComplement S ∅
-- Mathlib.Order.Basic
forall_ge_imp_ne_iff_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a ≤ c → c ≠ b) ↔ b < a
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instReflBEqPoly : ReflBEq Lean.Grind.Linarith.Poly
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_fac_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') {Z : CategoryTheory.Functor C H} (h : L.comp RF' ⟶ Z),
  CategoryTheory.CategoryStruct.comp α
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (RF.rightDerivedNatTrans RF' α α' W τ)) h) =
    CategoryTheory.CategoryStruct.comp τ (CategoryTheory.CategoryStruct.comp α' h)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_unique : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hE : CompleteSpace E] [inst_2 : Unique α] (f : α → E),
  ∫ (x : α), f x ∂μ = μ.real Set.univ • f default
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_left_mono : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightMono α] {a : α}, Monotone fun x => x + a
-- Lean.Level
Lean.Level.mvar.injEq : ∀ (a a_1 : Lean.LMVarId), (Lean.Level.mvar a = Lean.Level.mvar a_1) = (a = a_1)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmallSubtype : ∀ {α : Type v} [Std.Internal.Small α] {p : α → Prop}, Std.Internal.Small (Subtype p)
-- Init.Data.Vector.Lemmas
Vector.findSomeRev?_toArray : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  Array.findSomeRev? f xs.toArray = Vector.findSomeRev? f xs
-- Std.Sat.AIG.Basic
/-- Flip the polarity of `Ref` if `inv` is set.
 -/
Std.Sat.AIG.Ref.flip : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → Bool → aig.Ref
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.Const.getₘ : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (l : Std.DTreeMap.Internal.Impl α fun x => β) →
        (k : α) → (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).isSome = true → β
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_id_eq_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A X : C)
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.id (A ⟹ X)) = (CategoryTheory.ihom.ev A).app X
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Intermediate lemma for `unifTight_of_tendsto_Lp`.  -/
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.unifTight_of_tendsto_Lp_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : ℕ → α → β},
  p ≠ ⊤ →
    (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
      Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0) → MeasureTheory.UnifTight f p μ
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (F : CategoryTheory.Sheaf J (Type (max v v')))
  (s : ULift.{u, max v v'} (F.obj.obj X)),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app F)) s =
    J.uliftYonedaEquiv.symm s.down
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- In a finite-rank free module over a stably finite semiring, linear maps are inverse to
each other on one side if and only if they are inverse to each other on the other side.  -/
LinearMap.comp_eq_id_comm : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] [IsStablyFiniteRing R] {f g : M →ₗ[R] M}, f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.instCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A],
  CategoryTheory.AddMod.instCategory =
    { Hom := fun M N => M.Hom N, id := CategoryTheory.AddMod.id,
      comp := fun {X Y Z} f g => CategoryTheory.AddMod.comp f g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Analysis.Convex.Exposed
exposed_point_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.exposedPoints 𝕜 A ↔ x ∈ A ∧ ∃ l, ∀ y ∈ A, l y ≤ l x ∧ (l x ≤ l y → y = x)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating a vector by the angle to another vector gives the second vector if and only if the
norms are equal.  -/
Orientation.rotation_oangle_eq_iff_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.rotation (o.oangle x y)) x = y ↔ ‖x‖ = ‖y‖
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.coev_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom.coev A).app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
      ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f))
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayPanel : ProofWidgets.Component ProofWidgets.HtmlDisplayProps
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.HasTrivialRadical.mk : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.radical R L = ⊥ → LieAlgebra.HasTrivialRadical R L
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`.  -/
mem_nhdsLE_iff_exists_Ioc_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α}
  {s : Set α}, s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : AddMonoidAlgebra R M}, x.coeff = 0 ↔ x = 0
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_right_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α}, a ∉ s → Prod.mk a ⁻¹' s ×ˢ t = ∅
-- Mathlib.Probability.ConditionalProbability
/-- The axiomatic definition of conditional probability derived from a measure-theoretic one.  -/
ProbabilityTheory.cond_apply : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω},
  MeasurableSet s → ∀ (μ : MeasureTheory.Measure Ω) (t : Set Ω), μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (x : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (∀ (k : K) (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.push k f q → False) →
    (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.peek k f q → False) →
      (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.pop k f q → False) →
        (∀ (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.load a q → False) →
          (∀ (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.branch a q₁ q₂ → False) →
            (match x with
              | Turing.TM2.Stmt.push k f q => h_1 k f q
              | Turing.TM2.Stmt.peek k f q => h_2 k f q
              | Turing.TM2.Stmt.pop k f q => h_3 k f q
              | Turing.TM2.Stmt.load a q => h_4 a q
              | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
              | x => h_6 x) =
              h_6 x
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse_eq_inverse' : ∀ {M : Type u_2} {X : Type u_5} [inst : VAdd M X] {Y₁ : Type u_8} [inst_1 : VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂
-- Init.Data.BitVec.Lemmas
BitVec.toFin_abs : ∀ {w : ℕ} {x : BitVec w}, x.abs.toFin = if x.msb = true then Fin.ofNat (2 ^ w) (2 ^ w - x.toNat) else x.toFin
-- Lean.Server.References
/-- Index that allows efficiently looking up the imports of a module by module name.
Since the same module can be imported multiple times with different attributes,
each module name maps to an array of imports.
 -/
Lean.Server.ModuleImportIndex : Type
-- Lean.DocString.Syntax
/-- Ordered list  -/
Lean.Doc.Syntax.ol : Lean.ParserDescr
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_coe : Continuous Quaternion.coe
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_congr : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y Z T : C}
  {a₁ a₂ a₃ a₁₂ a₂₃ a : M} [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X T]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y T]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z T]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M T T]
  (α : CategoryTheory.Localization.SmallShiftedHom W X Y a₁) (β : CategoryTheory.Localization.SmallShiftedHom W Y Z a₂)
  (γ : CategoryTheory.Localization.SmallShiftedHom W Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃)
  (h : a₃ + a₂ + a₁ = a), (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
-- Mathlib.Order.Filter.Extr
IsMaxOn.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
  {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsMaxOn f s a → ∀ {g : α → γ}, IsMaxOn g s a → IsMaxOn (fun x => op (f x) (g x)) s a
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.add_zero : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.add a Lean.Grind.IntModule.OfNatModule.zero = a
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.ofScalar.injEq : ∀ {R : Type u_1} {X : Type u_2} (a a_1 : R), (FreeAlgebra.Pre.ofScalar a = FreeAlgebra.Pre.ofScalar a_1) = (a = a_1)
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.coe_toSeminorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜},
  ⇑f.toSeminorm = fun x => ‖f x‖
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, k ∈ m.alter k f ↔ (f m[k]?).isSome = true
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.inv.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 1).hom.app X.obj₁
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_exact.inj : ∀ {lhs : Bool} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {lhs_1 : Bool} {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs c₁ c₂ = Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.

See also `MulEquiv.mapSubgroup` which maps subgroups to their forward images.
 -/
MulEquiv.comapSubgroup : {G : Type u_1} → [inst : Group G] → {H : Type u_5} → [inst_1 : Group H] → G ≃* H → Subgroup H ≃o Subgroup G
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is minimized when
`f` and `g` antivary together. Stated by permuting the entries of `f`.  -/
Antivary.sum_smul_le_sum_comp_perm_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → ∑ i, f i • g i ≤ ∑ i, f (σ i) • g i
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.extract_gcd' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s t : Multiset α),
  (∃ x ∈ s, x ≠ 0) → s = Multiset.map (fun x => s.gcd * x) t → t.gcd = 1
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.forIn'.loop.match_3.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (x : 0 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.instMonoFunctorTypeι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F), CategoryTheory.Mono G.ι
-- Mathlib.Order.SuccPred.Archimedean
strictAntiOn_of_lt_pred : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f a < f (Order.pred a)) → StrictAntiOn f s
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.coeff.congr_simp : ∀ {𝕜 : 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 I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_9 : (x : M) → AddCommGroup (V x)]
  [inst_10 : (x : M) → Module 𝕜 (V x)] [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V]
  {ι : Type u_7} {s s_1 : ι → (x : M) → V x} (e_s : s = s_1) {u u_1 : Set M} (e_u : u = u_1) {n n_1 : WithTop ℕ∞}
  (e_n : n = n_1) (hs : IsLocalFrameOn I F n s u) (i i_1 : ι), i = i_1 → ∀ (x : M), hs.coeff i x = ⋯.coeff i_1 x
-- Mathlib.Data.Real.Basic
Real.instMonoidWithZero : MonoidWithZero ℝ
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks : ∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (P : CategoryTheory.Functor Dᵒᵖ (Type u_2)) {X : C} (R : CategoryTheory.Presieve X) [R.HasPairwisePullbacks]
  [F.PreservesPairwisePullbacks R],
  CategoryTheory.Presieve.IsSheafFor (F.op.comp P) R ↔
    CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.map F R)
-- Mathlib.Data.Finset.Sum
Finset.map_inl_disjUnion_map_inr : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β),
  (Finset.map Function.Embedding.inl s).disjUnion (Finset.map Function.Embedding.inr t) ⋯ = s.disjSum t
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_mem_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b ∈ Set.Ioc a (a + p)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_uIcc_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.uIcc (Fin.castAdd m i) (Fin.castAdd m j) = Set.uIcc i j
-- Mathlib.Algebra.Order.UpperLower
_private.Mathlib.Algebra.Order.UpperLower.0.LowerSet.one_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s : LowerSet α), 1 * s = s
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.instPseudoMetricSpace.eq_1 : ∀ {α : Type u_1} [inst : PseudoMetricSpace α],
  MulOpposite.instPseudoMetricSpace = PseudoMetricSpace.induced MulOpposite.unop inst
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The first projection from the product.  -/
CategoryTheory.SemiCartesianMonoidalCategory.fst : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ X
-- Lean.Elab.DocString
Lean.Doc.CodeSuggestion.mk.sizeOf_spec : ∀ (role : Lean.Name) (args moreInfo : Option String),
  sizeOf { role := role, args := args, moreInfo := moreInfo } = 1 + sizeOf role + sizeOf args + sizeOf moreInfo
-- Lean.Meta.CtorRecognizer
/-- If `e` is a constructor application or a builtin literal defeq to a constructor application,
then return the corresponding `ConstructorVal`.
 -/
Lean.Meta.isConstructorApp? : Lean.Expr → Lean.MetaM (Option Lean.ConstructorVal)
-- Lean.Elab.AutoBound
Lean.Elab.checkValidAutoBoundImplicitName : Lean.Name → Bool → Bool → Except Lean.MessageData Bool
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
/-- Cyclotomic polynomials are always nonnegative on inputs one or more.  -/
Polynomial.cyclotomic_nonneg : ∀ (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  1 ≤ x → 0 ≤ Polynomial.eval x (Polynomial.cyclotomic n R)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.multiset_prod_le_inf : ∀ {R : Type u} [inst : CommSemiring R] {s : Multiset (Ideal R)}, s.prod ≤ s.inf