mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero.  -/
hasFDerivAt_exp_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸], HasFDerivAt NormedSpace.exp 1 0
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.counit_comp : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : AddCommMonoid A} {inst_2 : Module R A} {inst_3 : AddCommMonoid B} {inst_4 : Module R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : CoalgHomClass F R A B]
  (f : F), CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_finitary : ∀ {α : Type u_1} {E I : Set α}, (Matroid.uniqueBaseOn I E).Finitary
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.takeAsArray`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.takeAsArray.go : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → ℕ → Array α → MLList m α → m (Array α)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instFieldFiniteResidueField : (K : Type u_1) →
  [inst : LinearOrder K] →
    [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → Field (ArchimedeanClass.FiniteResidueField K)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getPhase : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m Aesop.PhaseName
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} [MeasureTheory.SFinite μ],
  t ⊆ μ.sigmaFiniteSetᶜ → μ t = 0 ∨ μ t = ⊤
-- Mathlib.Data.Set.Prod
Set.pi_inter_distrib : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t t₁ : (i : ι) → Set (α i)},
  (s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁
-- Mathlib.Order.PrimeIdeal
/-- An ideal `I` is prime if its complement is a filter.
 -/
Order.Ideal.IsPrime : {P : Type u_1} → [inst : Preorder P] → Order.Ideal P → Prop
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- The supremum of a directed family of commutative subsemigroups is commutative.  -/
Subsemigroup.instIsMulCommutative_iSup : ∀ {M : Type u_2} [inst : Mul M] {ι : Type u_3} [inst_1 : Preorder ι] [IsDirectedOrder ι] (S : ι →o Subsemigroup M)
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), PowerSeries.monomial n = MvPowerSeries.monomial fun₀ | () => n
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraph.congr_simp : ∀ {α : Type u_1} {V : Type u_2} {A A_1 : Matrix V V α} (e_A : A = A_1) [inst : MulZeroOneClass α]
  [inst_1 : Nontrivial α] (h : A.IsAdjMatrix), h.toGraph = ⋯.toGraph
-- Init.Data.Order.MinMaxOn
maxOn_eq_minOn : ∀ {β : Type u_1} {α : Sort u_2} [le : LE β] [inst : DecidableLE β] {f : α → β} {x y : α}, maxOn f x y = minOn f x y
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_mul_inv_iff₀'` for a version with multiplication on the other side.  -/
lt_mul_inv_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (a < b * c⁻¹ ↔ a * c < b)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instBEqOfLawfulEqCmp : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → [(k : α) → BEq (β k)] → BEq (Std.DTreeMap α β cmp)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux0.eq_2 : ∀ (n : ℕ), n.succ.digitsAux0 = [n + 1]
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ i, c.Rel i j) (i j : ι) (hij : c.Rel j i),
  (HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = HomologicalComplex.homotopyCofiber.inlX φ i j hij
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_symm_X : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  matPolyEquiv.symm Polynomial.X = Matrix.diagonal fun x => Polynomial.X
-- Mathlib.Data.Int.ModEq
Int.mod_mul_left_mod : ∀ (a b c : ℤ), a % (b * c) % c = a % c
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_pos : ∀ (m : Multiset ℕ), 0 < m.multinomial
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.of_α : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C], ↑(CategoryTheory.Cat.of C) = C
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extendOfIsometry_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : Eₗ),
  (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm) x = ((e₂ ∘ₛₗ ↑f).extendOfNorm e₁) x
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_union_congr_left : ∀ {α : Type u_2} {M : Matroid α} {X Y X' : Set α}, M.closure X = M.closure X' → M.closure (X ∪ Y) = M.closure (X' ∪ Y)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C),
  (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.Equivalence.congrLeft.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  e.congrLeft =
    { functor := (CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse,
      inverse := (CategoryTheory.Functor.whiskeringLeft C D E).obj e.functor,
      unitIso := CategoryTheory.NatIso.ofComponents (fun F => (e.funInvIdAssoc F).symm) ⋯,
      counitIso := CategoryTheory.NatIso.ofComponents (fun F => e.invFunIdAssoc F) ⋯, functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.star_mem_resolventSet_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : InvolutiveStar R]
  [inst_4 : StarRing A] [StarModule R A] {r : R} {a : A}, star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
-- Lean.Elab.MutualDef
/-- Builds the view of a `where ... finally` section in a `declVal` syntax.  -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.declValToWhereFinally : Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.WhereFinallyView
-- Lean.Util.Sorry
/-- Returns `true` if the expression is of the form `sorryAx _ false ..`.  -/
Lean.Expr.isNonSyntheticSorry : Lean.Expr → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.any.eq_def : ∀ {α : Type u_1} (p : α → Bool) (x : RBTree.RBNode α),
  RBTree.RBNode.any p x =
    match x with
    | RBTree.RBNode.nil => false
    | RBTree.RBNode.node c l v r => p v || RBTree.RBNode.any p l || RBTree.RBNode.any p r
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
midpoint_le_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E}, midpoint k a b ≤ a ↔ b ≤ a
-- Mathlib.Data.Fintype.Basic
Multiset.map_univ_val_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (e : α ≃ β),
  Multiset.map (⇑e) Finset.univ.val = Finset.univ.val
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of the forward direction of `linearIndepOn_range_iff`. -/
LinearIndependent.of_linearIndepOn_range : ∀ {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {ι : Type u_6} {f : ι → ι'},
  Function.Injective f → ∀ (g : ι' → M), LinearIndepOn R g (Set.range f) → LinearIndependent R (g ∘ f)
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `splitAt`. (Can also be used in lieu of `splitAt` if you know the
index is within the range of the data structure.)

```
splitAtAux {a, b, c, d} 2 = ({a, b}, {c, d})
splitAtAux {a, b, c, d} 5 = ({a, b, c, d}, ∅)
```  -/
Ordnode.splitAtAux : {α : Type u_1} → Ordnode α → ℕ → Ordnode α × Ordnode α
-- Init.Data.BitVec.Bitblast
/-- A recursive definition of division for bit blasting, in terms of a shift-subtraction circuit.  -/
BitVec.divRec : {w : ℕ} → ℕ → BitVec.DivModArgs w → BitVec.DivModState w → BitVec.DivModState w
-- Mathlib.Algebra.Order.Group.End
OrderHom.mul_eq_comp : ∀ {α : Type u_1} [inst : Preorder α] (f g : α →o α), f * g = f.comp g
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
_private.Std.Tactic.BVDecide.LRAT.Internal.Assignment.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_4 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_4 ()
-- Mathlib.Data.Finmap
Finmap.insert_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : AList β),
  Finmap.insert a b s.toFinmap = (AList.insert a b s).toFinmap
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_add : ∀ (R : Type u_1) [inst : CommSemiring R] (p m n : ℕ) [inst_1 : ExpChar R p],
  iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.write_nth : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (b : Γ) (T : Turing.Tape Γ) {i : ℤ},
  (Turing.Tape.write b T).nth i = if i = 0 then b else T.nth i
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.altitudeFoot i = s_1.altitudeFoot i_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.MemLp.meas_ge_lt_top' : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {f : α → E},
  MeasureTheory.MemLp f p μ → p ≠ 0 → p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → μ {x | ε ≤ ↑‖f x‖₊} < ⊤
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.ofNat : ℕ → Turing.PartrecToTM2.Γ'
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) (n : ℕ), ⋯.addUnit = n • h.addUnit
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_5.splitter : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {x y : (CategoryTheory.WithTerminal C)ᵒᵖ} →
      (motive : (x ⟶ y) → Sort u_3) →
        (x_1 : x ⟶ y) → ((f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)) → motive x_1
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : C} (h : A₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃))
      (CategoryTheory.CategoryStruct.comp (hf₁.fst' f₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) h
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A point of a sphere that differs from another point of the sphere is not its center.  -/
EuclideanGeometry.Sphere.ne_center_of_mem_of_mem_of_ne : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p q : P}, p ∈ s → q ∈ s → p ≠ q → p ≠ s.center
-- Mathlib.Order.Filter.Lift
Filter.lift'_lift_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {h : Set β → Set γ},
  Monotone g → (f.lift g).lift' h = f.lift fun s => (g s).lift' h
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Order.LiminfLimsup
Filter.iInf_le_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α}, ⨅ n, u n ≤ Filter.liminf u f
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.distrib_lattice_lemma : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] [FaithfulSMul M X]
  {P Q R : { P // IsLprojection X P }}, (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.size = t.size ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.hom_inj : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → Function.Injective ⇑(algebraMap O R)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
IsLocalizedModule.mapExtendScalars.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_4} {N' : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_6)
  [inst_11 : CommSemiring Rₛ] [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N']
  [inst_15 : IsScalarTower R Rₛ M'] [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ],
  IsLocalizedModule.mapExtendScalars S f g Rₛ =
    ↑(LinearEquiv.restrictScalars R (LinearMap.extendScalarsOfIsLocalizationEquiv S Rₛ)) ∘ₗ IsLocalizedModule.map S f g
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_complex_ofReal : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℝ},
  ∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)
-- Mathlib.Topology.VectorBundle.Basic
/-- Forward map of `Bundle.Trivialization.continuousLinearEquivAt` (only propositionally equal),
defined everywhere (`0` outside domain).  -/
Bundle.Trivialization.continuousLinearMapAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_7 : (x : B) → TopologicalSpace (E x)] →
                        [FiberBundle F E] →
                          (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                            [Bundle.Trivialization.IsLinear R e] → (b : B) → E b →L[R] F
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.rev (Finset.Ioo i j) = Finset.Ioo j.rev i.rev
-- Mathlib.Logic.Equiv.Set
Equiv.eq_image_iff_symm_image_eq : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β), t = ⇑e '' s ↔ ⇑e.symm '' t = s
-- Mathlib.Algebra.Group.Defs
mul_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = n • m • a
-- Mathlib.Analysis.Complex.Circle
Circle.norm_smul : ∀ {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (u : Circle) (v : E), ‖u • v‖ = ‖v‖
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_eq_sum_factorization : ∀ {n : ℕ}, ArithmeticFunction.cardFactors n = n.factorization.sum fun x k => k
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- This lemma demonstrates the origin of the `foldl` name.  -/
CliffordAlgebra.foldl_prod_map_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (l : List M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N),
  ((CliffordAlgebra.foldl Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = List.foldl (fun m n => (f n) m) n l
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.HasCylinder.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K K_1 : HomologicalComplex C c) (e_K : K = K_1)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)], K.HasCylinder = K_1.HasCylinder
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorCotangentOfFlat_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T]
  (t : T) (x : P.Cotangent),
  (P.tensorCotangentOfFlat T) (t ⊗ₜ[R] x) = t • (Algebra.Extension.Cotangent.map (Algebra.Extension.toBaseChange T)) x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?_mem : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α}, RBTree.RBNode.upperBound? cut t = some x → x ∈ t
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.topIso_inv_app_hom_apply : ∀ (X : SSet) (X_1 : SimplexCategoryᵒᵖ) (x : X.obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.topIso X).inv.app X_1)) x = ⟨x, trivial⟩
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.instNonemptyElemSetOfPredAndIsFlatLeInterE : ∀ {α : Type u_2} {M : Matroid α} {X : Set α}, Nonempty ↑{F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The category of `T`-structured arrows with domain `S : D` (here `T : C ⥤ D`),
has as its objects `D`-morphisms of the form `S ⟶ T Y`, for some `Y : C`,
and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
 -/
CategoryTheory.StructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → D → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.Analysis.Convex.Exposed
IsExposed.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : Module 𝕜 E] {A B : Set E},
  IsExposed 𝕜 A B → Convex 𝕜 A → Convex 𝕜 B
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {M N : QuadraticModuleCat R} (f g : M ⟶ N),
  QuadraticModuleCat.Hom.toIsometry f = QuadraticModuleCat.Hom.toIsometry g → f = g
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a : α),
  ⇑e '' Set.Iio a = Set.Iio (e a)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.le_op_iff : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S₁ : Subsemiring Rᵐᵒᵖ} {S₂ : Subsemiring R}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsTopologicalAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.parse : Lean.TSyntax `mcasesPat → Lean.MacroM Lean.Parser.Tactic.MCasesPat
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_eq.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} (hst : s = t),
  SubMulAction.ofFixingSubgroup_of_eq M hst =
    {
      toFun := fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨x, ⋯⟩,
      map_smul' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.IsValidSearchFrom.splitFromSteps_eq_extend_split : ∀ {s : String.Slice} {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] (l : List (String.Slice.Pattern.SearchStep s))
  (pos pos' : s.Pos) (h₀ : pos ≤ pos'),
  (∀ (p : s.Pos), pos ≤ p → p < pos' → ¬String.Slice.Pattern.Model.MatchesAt pat p) →
    String.Slice.Pattern.Model.IsValidSearchFrom pat pos' l →
      String.Slice.Pattern.Model.splitFromSteps✝ pos l = String.Slice.Pattern.Model.split pat pos pos' h₀
-- Lean.Server.GoTo
Lean.Server.GoToContext.originInfo? : Lean.Server.GoToContext → Option Lean.Elab.Info