mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Spectrum.Basic
AlgEquivClass.toAlgEquiv.congr_simp : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B]
  [inst_6 : AlgEquivClass F R A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.zeroUnique : (G : Type u_2) → [inst : Group G] → Unique ↑(Equiv.Perm.vectorsProdEqOne G 0)
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.Raw.get! : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [Hashable α] → [LawfulBEq α] → Std.DHashMap.Raw α β → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.homOfPair.val : ∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (t : X) (g : G),
  ↑(CategoryTheory.ActionCategory.homOfPair t g) = g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_sub_nat_mul_pi : ∀ (x : ℂ) (n : ℕ), Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `f : X ⟶ Y` satisfies `W f`, then `f` is a transfinite composition of shape `Fin 2`
of morphisms in `W`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofMem : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (f : X ⟶ Y) → W f → W.TransfiniteCompositionOfShape (Fin 2) f
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_37 : HSub Std.Time.Week.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = Option.any (fun x => (f k x).isSome) (m.get? k)
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β},
  (∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j)) → Set.SurjOn f s (⋃ i, ⋃ j, t i j)
-- Init.Data.Vector.Lemmas
Vector.exists_of_mem_flatten : ∀ {α : Type u_1} {n n_1 : ℕ} {xss : Vector (Vector α n) n_1} {xs : α}, xs ∈ xss.flatten → ∃ ys ∈ xss, xs ∈ ys
-- Mathlib.Order.SuccPred.Limit
/-- See `not_isPredPrelimit_iff_pred_eq` for a version that states that `a` is a predecessor of a
value other than itself.  -/
Order.mem_range_pred_of_not_isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  ¬Order.IsPredPrelimit a → a ∈ Set.range Order.pred
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_smul : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] {R : Type u_10}
  [inst_6 : Monoid R] [inst_7 : DistribMulAction R V2] [inst_8 : SMulCommClass k R V2] (c : R) (f : P1 →ᵃ[k] V2),
  ⇑(c • f) = c • ⇑f
-- Mathlib.Tactic.FBinop
/-- Tree recording the structure of the `fbinop%` expression.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsReflexivePair.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B} (s : B ⟶ A),
  CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B →
    CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B → CategoryTheory.IsReflexivePair f g
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.ZoneRules.mk.inj : ∀ {initialLocalTimeType : Std.Time.TimeZone.LocalTimeType} {transitions : Array Std.Time.TimeZone.Transition}
  {transitionRule : Option Std.Time.TimeZone.RecurringRule} {initialLocalTimeType_1 : Std.Time.TimeZone.LocalTimeType}
  {transitions_1 : Array Std.Time.TimeZone.Transition} {transitionRule_1 : Option Std.Time.TimeZone.RecurringRule},
  { initialLocalTimeType := initialLocalTimeType, transitions := transitions, transitionRule := transitionRule } =
      { initialLocalTimeType := initialLocalTimeType_1, transitions := transitions_1,
        transitionRule := transitionRule_1 } →
    initialLocalTimeType = initialLocalTimeType_1 ∧ transitions = transitions_1 ∧ transitionRule = transitionRule_1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
AEStronglyMeasurable.stronglyMeasurableAtFilter_of_mem : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {l : Filter α} {f : α → β}
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict s) → s ∈ l → StronglyMeasurableAtFilter f l μ
-- Init.Data.Array.Lemmas
Array.contains_eq_any_beq : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : α}, xs.contains a = xs.any fun x => a == x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.homQuotientZSMulOfHom.eq_1 : ∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (f : A →+ B) (n : ℤ),
  QuotientAddGroup.homQuotientZSMulOfHom f n =
    QuotientAddGroup.lift (zsmulAddGroupHom n).range ((QuotientAddGroup.mk' (zsmulAddGroupHom n).range).comp f) ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ) (L : Filter (E × E)), HasFDerivAtFilter (↑z) 0 L
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M') (s : Set M) (x : M),
  mfderiv[s] f x =
    if MDiffAt[s] f x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
    else 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (k : α) (v : β k)
  (l : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match ⟨k, v⟩ :: l with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_2 k v l
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y))
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y) =
    Y.presheaf.stalkSpecializes ⋯
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.synthOrder : Lean.Meta.SynthInstance.Instance → Array ℕ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.roots 1 = ∅
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take.eq_3 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (n_2 : ℕ) (q : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h q).take n_2.succ = SimpleGraph.Walk.cons h (q.take n_2)
-- Mathlib.Topology.DiscreteSubset
Topology.IsInducing.isDiscrete_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  [DiscreteTopology X], Topology.IsInducing f → IsDiscrete (Set.range f)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodAssoc_symm_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : α × β × γ), (Equiv.prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.2)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instFunLikeContMDiffMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : Monoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'],
  instFunLikeContMDiffMonoidMorphism = { coe := fun a => (↑a.toMonoidHom).toFun, coe_injective := ⋯ }
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T}
  [P.ContainsIdentities] [P.RespectsIso], P.overObj.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_iff_isChain`. -/
List.IsChain.sortedGE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.IsChain (fun x1 x2 => x1 ≥ x2) l → l.SortedGE
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_impl_2 : {σ : Type} → Lean.EnvExtension σ → Lean.Environment → (σ → σ) → Array Lean.EnvExtensionState
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.IsCocontinuous.iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F G : CategoryTheory.Functor C D} (e : F ≅ G),
  F.IsCocontinuous J K ↔ G.IsCocontinuous J K
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.eq_def : ∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory C)
  (x_1 : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C x x_1 =
    match x, x_1 with
    | CategoryTheory.FreeMonoidalCategory.of a, x =>
      CategoryTheory.Iso.refl
        (((CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj (CategoryTheory.FreeMonoidalCategory.of a)).obj x)
    | CategoryTheory.FreeMonoidalCategory.unit, x =>
      CategoryTheory.MonoidalCategoryStruct.rightUnitor
        (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := x.as })
    | X.tensor a, n =>
      (CategoryTheory.MonoidalCategoryStruct.associator
            (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as }) X a).symm ≪≫
        CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n) a ≪≫
          CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C a { as := X.normalizeObj n.as }
-- Mathlib.Algebra.Opposites
/-- The element of `α` represented by `x : αᵐᵒᵖ`.  -/
MulOpposite.unop : {α : Type u_1} → αᵐᵒᵖ → α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  (Std.DHashMap.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback
-- Mathlib.Algebra.Order.Floor.Ring
/-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is.  -/
Mathlib.Meta.Positivity.evalNatCeil : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.Complex.Periodic
/-- One-sided inverse of `qParam h`.  -/
Function.Periodic.invQParam : ℝ → ℂ → ℂ
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.liftNCAlgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f f_1 : A →ₐ[R] B)
  (e_f : f = f_1) (g g_1 : M →* B) (e_g : g = g_1) (h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)),
  MonoidAlgebra.liftNCAlgHom f g h_comm = MonoidAlgebra.liftNCAlgHom f_1 g_1 ⋯
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceEq : Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.AdjoinRoot
/-- The surjective algebra morphism `R[X]/(minpoly R x) → R[x]`.
If `R` is an integrally closed domain and `x` is integral, this is an isomorphism,
see `minpoly.equivAdjoin`.  -/
AdjoinRoot.Minpoly.toAdjoin : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (x : S) → AdjoinRoot (minpoly R x) →ₐ[R] ↥R[x]
-- Init.Data.List.Range
List.range'_append : ∀ {s m n step : ℕ}, List.range' s m step ++ List.range' (s + step * m) n step = List.range' s (m + n) step
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.id_comp : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), AffineIsometry.id.comp f = f
-- Mathlib.Order.RelClasses
/-- Set notation form of `eq_of_le_of_not_lt'` -/
eq_of_subset_of_not_ssubset' : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → ¬b ⊂ a → a = b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_div_iff₀'` for a version with multiplication on the other side.  -/
lt_div_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)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.macroExpansion.inj : ∀ {macroName : Lean.Name} {stx stx' : Lean.Syntax} {nested : FBinopElab.Tree✝} {macroName_1 : Lean.Name}
  {stx_1 stx'_1 : Lean.Syntax} {nested_1 : FBinopElab.Tree✝},
  FBinopElab.Tree.macroExpansion✝ macroName stx stx' nested =
      FBinopElab.Tree.macroExpansion✝ macroName_1 stx_1 stx'_1 nested_1 →
    macroName = macroName_1 ∧ stx = stx_1 ∧ stx' = stx'_1 ∧ nested = nested_1
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- An injective linear map between finite-dimensional modules of equal rank
is a linear equivalence.

Unlike `LinearEquiv.ofFinrankEq` (which creates an *abstract* linear equivalence from `V` to `V'`),
this lemma improves a *given* injective linear map to a linear equivalence.
 -/
LinearEquiv.ofInjectiveOfFinrankEq : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {V' : Type u_1} →
            [inst_3 : AddCommGroup V'] →
              [inst_4 : Module K V'] →
                [FiniteDimensional K V'] →
                  (f : V →ₗ[K] V') → Function.Injective ⇑f → Module.finrank K V = Module.finrank K V' → V ≃ₗ[K] V'
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.withSimpGlobalConfig : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_toRegular : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : α), ↑(Heyting.Regular.toRegular a) = aᶜᶜ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a))
  (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryLE?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryLE?.go k best l
      | Ordering.eq => some ⟨ky, y⟩
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLE?.go k (some ⟨ky, y⟩) r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} (h : t.WF) {f : Option (β k) → Option (β k)},
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl = (f (t.get? k)).isSome
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.as_sum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p = ∑ v ∈ p.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_def : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] (p : Polynomial R)
  [inst_3 : Decidable (p = 0)], p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.evenKernel.eq_1 : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.evenKernel a x = ⋯.lift a
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ker_unitGroupToResidueFieldUnits : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K),
  A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
-- Init.Prelude
/-- Parses using another parser `declName`, which can be either
a `Parser` or `ParserDescr`.  -/
Lean.ParserDescr.parser : Lean.Name → Lean.ParserDescr
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.right_of_add : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f (n + m) x → Function.IsPeriodicPt f n x → Function.IsPeriodicPt f m x
-- Batteries.Data.Fin.Lemmas
Fin.find?_succ : ∀ {n : ℕ} {p : Fin (n + 1) → Bool},
  Fin.find? p = if p 0 = true then some 0 else Option.map Fin.succ (Fin.find? fun x => p x.succ)
-- Lean.Parser.Command
Lean.Parser.Command.inductive.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.ParamKind.mk.inj : ∀ {name : Lean.Name} {bInfo : Lean.BinderInfo} {defVal : Option Lean.Expr} {isAutoParam : Bool} {name_1 : Lean.Name}
  {bInfo_1 : Lean.BinderInfo} {defVal_1 : Option Lean.Expr} {isAutoParam_1 : Bool},
  { name := name, bInfo := bInfo, defVal := defVal, isAutoParam := isAutoParam } =
      { name := name_1, bInfo := bInfo_1, defVal := defVal_1, isAutoParam := isAutoParam_1 } →
    name = name_1 ∧ bInfo = bInfo_1 ∧ defVal = defVal_1 ∧ isAutoParam = isAutoParam_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List α), (t₁.insertMany l).Equiv (t₂.insertMany l)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_omega0 : Cardinal.preAleph Ordinal.omega0 = Cardinal.aleph0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.equivMapOfInjective.eq_1 : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (S : AddSubmonoid M) (f : M →+ N)
  (hf : Function.Injective ⇑f), S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_rightUnitor_inv_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.rightUnitor f).inv.1 = (CategoryTheory.Bicategory.rightUnitor f.1).inv
-- Mathlib.RingTheory.Extension.Basic
/-- Construct `Extension` from a surjective algebra homomorphism.  -/
Algebra.Extension.ofSurjective : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Type w} →
            [inst_3 : CommRing P] →
              [inst_4 : Algebra R P] → (f : P →ₐ[R] S) → Function.Surjective ⇑f → Algebra.Extension R S
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_injective : Function.Injective Ordinal.toZFSet
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (pos : s.Pos) → none = some pos → motive (some pos))
  (h_2 : none = none → motive none),
  (match hd : none with
    | some pos => h_1 pos hd
    | none => h_2 hd) =
    h_2 ⋯
-- Init.Data.Int.Lemmas
Int.sub_add_cancel : ∀ (a b : ℤ), a - b + b = a
-- Mathlib.Order.Preorder.Chain
Flag.mem_iff_forall_le_or_ge : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s : Flag α}, a ∈ s ↔ ∀ ⦃b : α⦄, b ∈ s → a ≤ b ∨ b ≤ a
-- Mathlib.Data.Finset.Image
/-- **Alias** of the forward direction of `Finset.image_eq_iff_surjOn_mapsTo`. -/
Set.SurjOn.finsetImage_eq_of_mapsTo : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Finset.image f s = t → Set.SurjOn f ↑s ↑t ∧ Set.MapsTo f ↑s ↑t
-- Lean.Data.Json.Basic
Lean.Json.Structured : Type
-- Init.Data.List.Lemmas
List.getElem_filter : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ} (h : i < (List.filter p xs).length),
  p (List.filter p xs)[i] = true
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_add : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] {f : α → β} (v₁ v₂ : β →₀ M)
  (hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)) (hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support))
  (hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)),
  Finsupp.comapDomain f (v₁ + v₂) hv₁₂ = Finsupp.comapDomain f v₁ hv₁ + Finsupp.comapDomain f v₂ hv₂