mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_2.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_3 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Init.Data.Vector.Attach
Vector.pmap_reverse : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
  (H : ∀ a ∈ xs.reverse, P a), Vector.pmap f xs.reverse H = (Vector.pmap f xs ⋯).reverse
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together on `s`, is unchanged by a permutation if and only if `f ∘ σ` and `g`
monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε},
  MeasureTheory.Integrable f μ → ∀ {c : ENNReal}, c ≠ ⊤ → MeasureTheory.Integrable f (c • μ)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {m n : ℕ} (_h : m ≤ n) (a a_1 : L.BoundedFormula α m),
  a = a_1 → FirstOrder.Language.BoundedFormula.castLE _h a = FirstOrder.Language.BoundedFormula.castLE _h a_1
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.LeanDiagnosticTag.goalsAccomplished.sizeOf_spec : sizeOf Lean.Lsp.LeanDiagnosticTag.goalsAccomplished = 1
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE : ∀ (p : ℤ), (ComplexShape.embeddingUpIntGE p).IsTruncGE
-- Mathlib.Algebra.Group.Defs
DivInvMonoid.toInv : {G : Type u} → [self : DivInvMonoid G] → Inv G
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.oneTruncation₂_map : ∀ {X Y : SSet.Truncated 2} (f : X ⟶ Y), SSet.oneTruncation₂.map f = SSet.OneTruncation₂.map f
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.single` as a `MonoidHom` from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`MonoidAlgebra.single`.  -/
MonoidAlgebra.singleHom : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [inst_1 : MulOneClass M] → R × M →* MonoidAlgebra R M
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.instMonoFShortComplexTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], CategoryTheory.Mono (K.shortComplexTruncLE e).f
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Every element in the fiber of `X` lies in some connected component of `X`.  -/
CategoryTheory.PreGaloisCategory.fiber_in_connected_component : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (x : (F.obj X).obj),
  ∃ Y i y,
    (CategoryTheory.ConcreteCategory.hom (F.map i)) y = x ∧
      CategoryTheory.PreGaloisCategory.IsConnected Y ∧ CategoryTheory.Mono i
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_bot_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.relIndex ⊥ = 1
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} {i : ℕ},
  (List.zipWithAll f as bs)[i]? =
    match as[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_descCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A)
  (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0)
  {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n)
      (CategoryTheory.CategoryStruct.comp (X.descCycles f g fg h x hx) h_1) =
    CategoryTheory.CategoryStruct.comp x h_1
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Y : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.Y✝ S
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.ofEquiv_σ : ∀ {α : Type u_1} {τ : Type u_4} [inst : TopologicalSpace α] (F : Ctop.Realizer α) (E : F.σ ≃ τ), (F.ofEquiv E).σ = τ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- Extension for the `positivity` tactic: `Real.log` of a natural number is always nonnegative.  -/
Mathlib.Meta.Positivity.evalLogNatCast : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Opposites
MulOpposite.unop_mul : ∀ {α : Type u_1} [inst : Mul α] (x y : αᵐᵒᵖ), MulOpposite.unop (x * y) = MulOpposite.unop y * MulOpposite.unop x
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates limits of shape `J` and `J ≌ J'`, then `F` creates limits of shape `J'`.  -/
CategoryTheory.createsLimitsOfShapeOfEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {J' : Type w₁} →
              [inst_3 : CategoryTheory.Category.{w'₁, w₁} J'] →
                (J ≌ J') →
                  (F : CategoryTheory.Functor C D) →
                    [CategoryTheory.CreatesLimitsOfShape J F] → CategoryTheory.CreatesLimitsOfShape J' F
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- **Alias** of the reverse direction of `Subalgebra.bot_eq_top_iff_rank_eq_one`. -/
Subalgebra.bot_eq_top_of_rank_eq_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [Nontrivial E] [Module.Free F E], Module.rank F E = 1 → ⊥ = ⊤
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The canonical isomorphism `X ≅ Spec Γ(X)` for an affine scheme.  -/
AlgebraicGeometry.Scheme.isoSpec : (X : AlgebraicGeometry.Scheme) →
  [AlgebraicGeometry.IsAffine X] → X ≅ AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The type of connected components of a simplicial set.  -/
SSet.π₀ : SSet → Type u
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mpullback_mlieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M]
  [inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'}
  {V W : (x : M') → TangentSpace I' x} {x₀ : M},
  MDiffAt (T% V) (f x₀) →
    MDiffAt (T% W) (f x₀) →
      ContMDiffAt I I' n f x₀ →
        minSmoothness 𝕜 2 ≤ n →
          VectorField.mpullback I I' f (VectorField.mlieBracket I' V W) x₀ =
            VectorField.mlieBracket I (VectorField.mpullback I I' f V) (VectorField.mpullback I I' f W) x₀
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey_eq_self : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.containsKey k l = true →
    (f (Std.Internal.List.getValue? k l)).isSome = true → (Std.Internal.List.Const.alterKey k f l).length = l.length
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.PreservesProjectiveObjects.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X : C}, CategoryTheory.Projective X → CategoryTheory.Projective (F.obj X)) → F.PreservesProjectiveObjects
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.snd_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R), (CategoryTheory.Comma.snd L R).obj X = X.right
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_neg_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  μ.transpose (-B) = -μ.transpose B
-- Mathlib.Algebra.Order.Module.Basic
sup_eq_half_smul_add_add_abs_sub : ∀ (R : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Invertible 2] [inst_2 : Lattice M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsOrderedAddMonoid M] (x y : M), x ⊔ y = ⅟2 • (x + y + |y - x|)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.prop_toSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C),
  Φ.prop (Φ.toSucc X)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.match_3.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  fuel = 0 →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_1 ()
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instCommMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : CommMonoid N],
  OneHom.instCommMonoid = { toMonoid := OneHom.instMonoid, mul_comm := ⋯ }
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.map_ringHom : ∀ {R : Type u} {S : Type u_1} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) {I : Ideal R}, Submodule.IsPrincipal I → Submodule.IsPrincipal (Ideal.map f I)
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `‖f a‖ ≤ B a`;
* `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
* the norm of `f'` is strictly less than `B'` whenever `‖f x‖ = B x`.

Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
to make this theorem work for piecewise differentiable functions.
 -/
image_norm_le_of_norm_deriv_right_lt_deriv_boundary' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        ‖f a‖ ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.faceι_ι : ∀ {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.boundary.faceι i) (SSet.boundary (n + 1)).ι = (SSet.stdSimplex.face {i}ᶜ).ι
-- Mathlib.Order.Filter.Pointwise
Filter.monoid.eq_1 : ∀ {α : Type u_2} [inst : Monoid α],
  Filter.monoid =
    { toMul := Filter.mulOneClass.toMul, mul_assoc := ⋯, toOne := Filter.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (↑↑f).toFun = ⇑f
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
/-- Given a morphism `s : Spec (.of Ω) ⟶ S` with image `s₀ : S` where `Ω` is a
separably closed field, this is the canonical map
`(pointSmallEtale s).fiber.obj X ⟶ X.hom ⁻¹' {s₀}` for `X : S.Etale`.  -/
AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage : {S : AlgebraicGeometry.Scheme} →
  {Ω : Type u} →
    [inst : Field Ω] →
      [inst_1 : IsSepClosed Ω] →
        (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) →
          {s₀ : ↥S} →
            s default = s₀ →
              {X : S.Etale} → (AlgebraicGeometry.Scheme.pointSmallEtale s).fiber.obj X → ↑(⇑X.hom ⁻¹' {s₀})
-- Init.Data.Float.Float32
instMinFloat32 : Min Float32
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCocircuit.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (e : α) (B : Set α), M.fundCocircuit e B = M✶.fundCircuit e (M✶.E \ B)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inr_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
      (CategoryTheory.Limits.PreservesPushout.iso G f g).hom =
    G.map (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_smul' : ∀ {K : Type u_4} {V : Type u_8} {V₂ : Type u_9} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (a : K), (a • f).range = ⨆ (_ : a ≠ 0), f.range
-- Mathlib.Algebra.Module.LinearMap.DivisionRing
LinearMap.range_smulRight_apply_of_surjective : ∀ {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : Module R M₁] {f : M →ₗ[R] R},
  Function.Surjective ⇑f → ∀ (x : M₁), (f.smulRight x).range = R ∙ x
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Iso.card_edgeFinset_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} (f : G ≃g G') [inst : Fintype ↑G.edgeSet]
  [inst_1 : Fintype ↑G'.edgeSet], G.edgeFinset.card = G'.edgeFinset.card
-- Lean.Environment
/-- `quotInit = true` if the command `init_quot` has already been executed for the environment, and
`Quot` declarations have been added to the environment. When the flag is set, the type checker can
assume that the `Quot` declarations in the environment have indeed been added by the kernel and
not by the user.
 -/
Lean.Kernel.Environment.quotInit : Lean.Kernel.Environment → Bool
-- Mathlib.Algebra.Algebra.Basic
/-- If `E` is an `F`-algebra, and there exists a bijective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also bijective.

NOTE: The same result can also be obtained if there are two `F`-linear maps from `F` to `E`,
one is injective, the other one is surjective. In this case, use
`injective_algebraMap_of_linearMap` and `surjective_algebraMap_of_linearMap` separately.  -/
bijective_algebraMap_of_linearMap : ∀ {F : Type u_1} {E : Type u_2} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E] (b : F →ₗ[F] E),
  Function.Bijective ⇑b → Function.Bijective ⇑(algebraMap F E)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).op = CategoryTheory.MonoidalCategoryStruct.tensorHom f.op g.op
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `pi_Lp.pseudo_emetric_space` so it can be used also for `p < 1`.  -/
PiLp.edist_comm : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  (f g : PiLp p β), edist f g = edist g f
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instIsMarkovKernelOfIsEmpty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty α]
  (κ : ProbabilityTheory.Kernel α β), ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_zero_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.zero)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_add_right : ∀ {a b c : ℤ}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.normal.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] (a : Λ),
  sizeOf (Turing.TM0to1.Λ'.normal a) = 1 + sizeOf a
-- Mathlib.Algebra.Order.Group.Basic
zsmul_le_zsmul_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α},
  0 < n → (n • a ≤ n • b ↔ a ≤ b)
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem set in dimension 1: if the derivative of a function is bounded by `C`,
then the function is `C`-Lipschitz. Version with `deriv` and `LipschitzWith`.  -/
lipschitzWith_of_nnnorm_deriv_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {C : NNReal}, Differentiable 𝕜 f → (∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C) → LipschitzWith C f
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for `applyAssignment.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processDelayed : (mvars : Array Lean.Expr) →
  (i : ℕ) → i < mvars.size → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul : ∀ {n a b c d : ℕ}, a ≡ b [MOD n] → c ≡ d [MOD n] → a * c ≡ b * d [MOD n]
-- Lean.Meta.HaveTelescope
Lean.Meta.instInhabitedSimpHaveResult.default : Lean.Meta.SimpHaveResult✝
-- Batteries.Lean.NameMapAttribute
Lean.instInhabitedNameMapAttributeImpl.default : {α : Type} → Lean.NameMapAttributeImpl α
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_zero_iff' : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) {X_1 Y_1 : CategoryTheory.Over Y} (g : X_1 ⟶ Y_1),
  (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).map g =
    CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Over.Hom.left g)) ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_map_app : ∀ (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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {X Y : C} (f : X ⟶ Y) (y : D),
  ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).map f).app y =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight y f
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_ext_iff' : ∀ {R : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : StarMul R] [inst_2 : CommRing S] [inst_3 : StarMul S]
  [inst_4 : Algebra S R] [inst_5 : StarModule S R] [Algebra.IsCentral S R] [IsCancelMulZero S]
  [Module.IsTorsionFree S R] (u v : ↥(unitary R)),
  (Unitary.conjStarAlgAut S R) u = (Unitary.conjStarAlgAut S R) v ↔ ∃ α, u = α • v
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true), f (Std.Internal.List.getKey k l h) = false)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.to_single_hom_ext_iff : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (HomologicalComplex.single V c j).obj A},
  f = g ↔ f.f j = g.f j