mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.single_mul_eq_updateRow_zero : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (i : l) (j : m) (r : α) (B : Matrix m n α),
  Matrix.single i j r * B = Matrix.updateRow 0 i (r • B.row j)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsLeft.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z : C} (i : X ⟶ Y), Q i → ∀ (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp i f)) → P.RespectsLeft Q
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.id : Lean.Meta.Grind.AC.Struct → ℕ
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.id_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  (x : CategoryTheory.Limits.ColimitPresentation.Total P),
  (CategoryTheory.CategoryStruct.id x).base = CategoryTheory.CategoryStruct.id x.fst
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.uncons?Impl : {m : Type u_1 → Type u_1} → {α : Type u_1} → MLList.MLListImpl✝ m α → Option (Option (α × MLList.MLListImpl✝ m α))
-- Mathlib.Condensed.Module
CondensedMod.hom_naturality_apply : ∀ (R : Type (u + 1)) [inst : Ring R] {X Y : CondensedMod R} (f : X ⟶ Y) {S T : CompHausᵒᵖ} (g : S ⟶ T)
  (x : ↑(X.obj.obj S)),
  (CategoryTheory.ConcreteCategory.hom (f.hom.app T)) ((CategoryTheory.ConcreteCategory.hom (X.obj.map g)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.obj.map g)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app S)) x)
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support is bounded below.  -/
Continuous.bddBelow_range_of_hasCompactSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [inst_4 : Zero α] {f : β → α}, Continuous f → HasCompactSupport f → BddBelow (Set.range f)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.erase.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.erase a = t_1.erase a_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insertIfNew k v)[a]? = if (k == a) = true ∧ k ∉ m then some v else m[a]?
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (i : ι) (m : M),
  (b.dualBasis i) m = (b.repr m) i
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_condExp : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [CompleteSpace E] (f : Ω → E)
  (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.Martingale (fun i => μ[f | ↑ℱ i]) ℱ μ
-- Mathlib.Algebra.Lie.Weights.IsSimple
_private.Mathlib.Algebra.Lie.Weights.IsSimple.0.LieAlgebra.IsKilling.chi_in_q_aux : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H))
  (χ : LieModule.Weight K (↥H) L) (x_χ m_α : L),
  x_χ ∈ LieModule.genWeightSpace L ⇑χ →
    ∀ (α : LieModule.Weight K (↥H) L),
      LieModule.Weight.toLinear K (↥H) L α ∈ q →
        LieModule.Weight.toLinear K (↥H) L χ + LieModule.Weight.toLinear K (↥H) L α ≠ 0 →
          LieModule.Weight.toLinear K (↥H) L χ - LieModule.Weight.toLinear K (↥H) L α ≠ 0 →
            LieModule.Weight.toLinear K (↥H) L χ ≠ 0 →
              ∀ (m_pos m_neg : L) (y : ↥H),
                ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆ →
                  ⁅x_χ, m_pos⁆ ∈ LieModule.genWeightSpace L (⇑χ + ⇑α) →
                    ⁅x_χ, m_neg⁆ ∈ LieModule.genWeightSpace L (⇑χ - ⇑α) →
                      LieModule.Weight.toLinear K (↥H) L χ ∈ q →
                        ⁅x_χ, m_α⁆ ∈ ⨆ α, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxcHasSize.eq_1 : Int8.instRxcHasSize = { size := fun lo hi => (hi.toInt + 1 - lo.toInt).toNat }
-- Mathlib.Data.Complex.Basic
Complex.im_surjective : Function.Surjective Complex.im
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.coe_cartan_eq_span : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H),
  H.toSubmodule = Submodule.span R (Set.range b.h)
-- Mathlib.Data.Finmap
/-- The singleton map.  -/
Finmap.singleton : {α : Type u} → {β : α → Type v} → (a : α) → β a → Finmap β
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlyingIso_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv
      (CategoryTheory.Subobject.mk f).arrow =
    f
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint over `F`, then their intersection is equal to `F`.
This is actually an equivalence if `A/F` and `B/F` are finite dimensional, and `A/F` is Galois,
see `IntermediateField.LinearDisjoint.iff_inf_eq_bot`.
 -/
IntermediateField.LinearDisjoint.inf_eq_bot : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B → A ⊓ B = ⊥
-- Mathlib.Data.Set.Monotone
AntitoneOn.monotone : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  AntitoneOn f s → Antitone (f ∘ Subtype.val)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Total.toListRev.congr_simp : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] (it it_1 : Std.Iter.Total β),
  it = it_1 → it.toListRev = it_1.toListRev
-- Mathlib.Order.Cover
CovBy.ne' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ⋖ a → a ≠ b
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.mk.injEq : ∀ (clsName : Lean.Name) (privateSpecs : Bool) (fieldImpls : Array (Lean.Name × Lean.Name))
  (thms : Array Lean.MethodSpecTheorem✝) (clsName_1 : Lean.Name) (privateSpecs_1 : Bool)
  (fieldImpls_1 : Array (Lean.Name × Lean.Name)) (thms_1 : Array Lean.MethodSpecTheorem✝),
  ({ clsName := clsName, privateSpecs := privateSpecs, fieldImpls := fieldImpls, thms := thms } =
      { clsName := clsName_1, privateSpecs := privateSpecs_1, fieldImpls := fieldImpls_1, thms := thms_1 }) =
    (clsName = clsName_1 ∧ privateSpecs = privateSpecs_1 ∧ fieldImpls = fieldImpls_1 ∧ thms = thms_1)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isMulRightInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → Group (α i)] [∀ (i : ι), MeasurableMul (α i)] [∀ (i : ι), (μ i).IsMulRightInvariant],
  (MeasureTheory.Measure.pi μ).IsMulRightInvariant
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all
`a, b, c`.

See also `ext_iff_inner_right_threefold` for when `x, y : E ⊗ F ⊗ G`.  -/
TensorProduct.ext_iff_inner_right_threefold' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)},
  x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) = inner 𝕜 y (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c))
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- Change the ground set of a matroid to some `R : Set α`. The independent sets of the restriction
are the independent subsets of the new ground set. Most commonly used when `R ⊆ M.E`,
but it is convenient not to require this. The elements of `R \ M.E` become 'loops'.  -/
Matroid.restrict : {α : Type u_1} → Matroid α → Set α → Matroid α
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The isomorphism between `F.mapCochainComplexPlus ⋙ CochainComplex.Plus.ι D`
and `CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex _` when `F : C ⥤ D`
is a functor which preserves zero morphisms  -/
CategoryTheory.Functor.mapCochainComplexPlusCompι : {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] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
              [inst_4 : F.PreservesZeroMorphisms] →
                F.mapCochainComplexPlus.comp (CochainComplex.Plus.ι D) ≅
                  (CochainComplex.Plus.ι C).comp (F.mapHomologicalComplex (ComplexShape.up ℤ))
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (op : Lean.Expr) (neutral? : Option Lean.Expr) (assocInst : Lean.Expr)
  (idempotentInst? commInst? neutralInst? : Option Lean.Expr) (nextId : ℕ) (vars : Lean.PArray Lean.Expr)
  (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr)
  (denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue : Lean.Meta.Grind.AC.Queue)
  (basis : List Lean.Meta.Grind.AC.EqCnstr) (diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck : Bool),
  sizeOf
      { id := id, type := type, u := u, op := op, neutral? := neutral?, assocInst := assocInst,
        idempotentInst? := idempotentInst?, commInst? := commInst?, neutralInst? := neutralInst?, nextId := nextId,
        vars := vars, varMap := varMap, denote := denote, denoteEntries := denoteEntries, queue := queue,
        basis := basis, diseqs := diseqs, recheck := recheck } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf op + sizeOf neutral? + sizeOf assocInst + sizeOf idempotentInst? +
                          sizeOf commInst? +
                        sizeOf neutralInst? +
                      sizeOf nextId +
                    sizeOf vars +
                  sizeOf varMap +
                sizeOf denote +
              sizeOf denoteEntries +
            sizeOf queue +
          sizeOf basis +
        sizeOf diseqs +
      sizeOf recheck
-- Qq.ForLean.ToExpr
instToExprMData_qq : Lean.ToExpr Lean.MData
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.SemanticTokensParams
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A dense open set `U : Opens X` is birational to `X`.  -/
AlgebraicGeometry.Scheme.Opens.birational_of_dense : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), Dense ↑U → (↑U).Birational X
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.HashMap.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.LinearAlgebra.Pi
Function.ExtendByZero.linearMap_apply : ∀ (R : Type u) {ι : Type x} {η : Type u_1} [inst : Semiring R] (s : ι → η) (f : ι → R) (a : η),
  (Function.ExtendByZero.linearMap R s) f a = Function.extend s f 0 a
-- Mathlib.GroupTheory.SpecificGroups.Alternating
instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton : (α : Type u_1) → [inst : Fintype α] → [inst_1 : DecidableEq α] → [Subsingleton α] → Unique ↥(alternatingGroup α)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.of_def : ∀ {I : Type u_1} [inst : DecidableEq I] (R : Type u_2) [inst_1 : CommSemiring R] (A : I → Type u_3)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {i : I},
  LinearAlgebra.FreeProduct.of R A = LinearAlgebra.FreeProduct.ι R A i
-- Mathlib.Computability.Reduce
/-- For many-one degrees `d₁` and `d₂`, `d₁ ≤ d₂` if the sets in `d₁` are many-one reducible to the
sets in `d₂`.
 -/
ManyOneDegree.instLE : LE ManyOneDegree
-- Mathlib.Order.Preorder.Chain
IsMaxChain.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α),
  IsMaxChain r s = (IsChain r s ∧ ∀ ⦃t : Set α⦄, IsChain r t → s ⊆ t → s = t)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  -Set.Ico a b = Set.Ioc (-b) (-a)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- The identity graded ring homomorphism from a graded ring to itself.  -/
GradedRingHom.id : {ι : Type u_1} → {A : Type u_2} → {σ : Type u_6} → [inst : Semiring A] → [inst_1 : SetLike σ A] → (𝒜 : ι → σ) → 𝒜 →+*ᵍ 𝒜
-- Init.Data.String.Bootstrap
String.Internal.isEmpty : String → Bool
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousLinearMap.toContinuousAffineMap_map_zero : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : TopologicalSpace W]
  (f : V →L[R] W), f.toContinuousAffineMap 0 = 0
-- Mathlib.Combinatorics.Matroid.Map
Matroid.IsBase.mapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {B : Set α},
  M.IsBase B → ∀ (f : α ↪ β), (M.mapEmbedding f).IsBase (⇑f '' B)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul_left : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M} {n m : ℕ},
  0 ≤ a → n ≤ m → n • a ≤ m • a
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.digamma_one_half : (1 / 2).digamma = -2 * Complex.log 2 - ↑Real.eulerMascheroniConstant
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.alternatingProd_append : ∀ {G : Type u_7} [inst : CommGroup G] (l₁ l₂ : List G),
  (l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_one_one_eq_X : ∀ {R : Type u_1} [inst : Semiring R], (SkewPolynomial.monomial 1) 1 = SkewPolynomial.X
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.comp_lift : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (f : L →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p], PerfectRing.lift i (f.comp i) p = f
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- A sentence saying every monic polynomial of degree `n` has a root.  -/
FirstOrder.Field.genericMonicPolyHasRoot : ℕ → FirstOrder.Language.ring.Sentence
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_finsuppSum : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  (f : ι →₀ N) (g : ι → N → AddMonoidAlgebra R M), (f.sum g).coeff = f.sum fun i n => (g i n).coeff
-- Init.Data.Array.Basic
List.toList_toArray : ∀ {α : Type u} {as : List α}, as.toArray.toList = as
-- Mathlib.Logic.Equiv.Set
Equiv.ofPreimageEquiv_apply : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
  (a : α), (Equiv.ofPreimageEquiv e) a = ↑((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_diff_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.diff m₂).contains k = true ↔ m₁.contains k = true ∧ ¬m₂.contains k = true
-- Mathlib.Topology.Piecewise
continuousOn_piecewise_ite' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s s' t : Set α}
  [inst_2 : (x : α) → Decidable (x ∈ t)],
  ContinuousOn f (s ∩ closure t) →
    ContinuousOn g (s' ∩ closure tᶜ) →
      s ∩ frontier t = s' ∩ frontier t → Set.EqOn f g (s ∩ frontier t) → ContinuousOn (t.piecewise f g) (t.ite s s')
-- Batteries.Data.String.Lemmas
String.lt_antisymm : ∀ {s₁ s₂ : String}, ¬s₁ < s₂ → ¬s₂ < s₁ → s₁ = s₂
-- Mathlib.GroupTheory.Index
AddSubgroup.index_inf_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, (H ⊓ K).index ≤ H.index * K.index
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.snd : ∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, (e.oadd n a).NFBelow b → a.NFBelow e.repr
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqArg.beq : Lean.IR.Arg → Lean.IR.Arg → Bool
-- Mathlib.Data.Multiset.Count
Multiset.nodup_iff_count_eq_one : ∀ {α : Type u_1} {s : Multiset α} [inst : DecidableEq α], s.Nodup ↔ ∀ a ∈ s, Multiset.count a s = 1
-- Mathlib.Analysis.Convex.Piecewise
/-- The piecewise function `(Set.Iic e).piecewise f g` of a function `f` decreasing and convex on
`Set.Iic e` and a function `g` increasing and convex on `Set.Ici e`, such that `f e = g e`, is
convex on the universal set.  -/
convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] [inst_7 : AddCommGroup β]
  [inst_8 : PartialOrder β] [IsOrderedAddMonoid β] [inst_10 : Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β},
  ConvexOn 𝕜 (Set.Iic e) f →
    ConvexOn 𝕜 (Set.Ici e) g →
      AntitoneOn f (Set.Iic e) → MonotoneOn g (Set.Ici e) → f e = g e → ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise f g)
-- Mathlib.Topology.Category.Sequential
Sequential.mk : (toTop : TopCat) → [is_sequential : SequentialSpace ↑toTop] → Sequential
-- Lean.Elab.Command
Lean.Elab.Command.State.scopes : Lean.Elab.Command.State → List Lean.Elab.Command.Scope
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernsteinApproximation.eq_1 : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)),
  bernsteinApproximation n f = ∑ k, bernstein n ↑k • ContinuousMap.const (↑unitInterval) (f (bernstein.z k))
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f: M → N` and `g: M' × N'` are immersions at `x` and `x'`, respectively,
then `f × g: M × N → M' × N'` is an immersion at `(x, x')`.  -/
Manifold.IsImmersionAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {E''' : Type u_4} {E'' : Type u}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E']
  [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E'']
  [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E'''] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {H' : Type u_8} [inst_10 : TopologicalSpace H'] {G : Type u_9} [inst_11 : TopologicalSpace G] {G' : Type u_10}
  [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_13 : TopologicalSpace M]
  [inst_14 : ChartedSpace H M] {M' : Type u_12} [inst_15 : TopologicalSpace M'] [inst_16 : ChartedSpace H' M']
  {N : Type u_13} [inst_17 : TopologicalSpace N] [inst_18 : ChartedSpace G N] {N' : Type u_14}
  [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {g : M' → N'}
  {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'],
  Manifold.IsImmersionAt I J n f x →
    Manifold.IsImmersionAt I' J' n g x' → Manifold.IsImmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x')
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_iInter_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VSub α β] (s : Set β) (t : ι → Set β),
  s -ᵥ ⋂ i, t i ⊆ ⋂ i, s -ᵥ t i
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.isOpen_iff_generate_Iic_compl : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {s : Set α},
  IsOpen s ↔ TopologicalSpace.GenerateOpen {t | ∃ a, (Set.Iic a)ᶜ = t} s
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_map_fst_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true ↔
    Std.Internal.List.containsKey k l₁ = true ∧ ¬Std.Internal.List.containsKey k l₂ = true
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getInductiveValFromMajor : Bool → Lean.Expr → Lean.Elab.Tactic.TacticM Lean.InductiveVal
-- Init.Prelude
MonadWithReader.mk : {ρ : outParam (Type u)} → {m : Type u → Type v} → ({α : Type u} → (ρ → ρ) → m α → m α) → MonadWithReader ρ m
-- Mathlib.Algebra.Star.Basic
star_eq_iff_star_eq : ∀ {R : Type u} [inst : InvolutiveStar R] {r s : R}, star r = s ↔ star s = r
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.instVAddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M N αᵃᵒᵖ
-- Init.Data.List.Basic
/-- Checks whether the first list is a contiguous sub-list of the second.

The relation `List.IsInfixOf` expresses this property with respect to logical equality.

Examples:
* `[2, 3].isInfixOf_internal [1, 2, 3, 4] = true`
* `[2, 3].isInfixOf_internal [1, 3, 2, 4] = false`
* `[2, 3].isInfixOf_internal [2, 3] = true`
* `[2, 3].isInfixOf_internal [1] = false`

 Used internally by the `cbv` tactic.
 -/
List.isInfixOf_internal : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- The closed form for the quaternion exponential on imaginary quaternions.  -/
Quaternion.exp_of_re_eq_zero : ∀ (q : Quaternion ℝ), q.re = 0 → NormedSpace.exp q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.Limits.colim.mapShortComplex_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
  {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone S.X₂) (c₃ : CategoryTheory.Limits.Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt)
  (g : c₂.pt ⟶ c₃.pt)
  (hf :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
  (hg :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g = CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
  (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₃ = c₃.pt
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback