mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_ciSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ᶠ (y : α) in nhds x, BddAbove (Set.range fun i => f i y)) →
    (∀ (i : ι), LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.mk.sizeOf_spec : ∀ (mctx : Lean.MetavarContext) (nextMacroScope : Lean.MacroScope) (ngen : Lean.NameGenerator)
  (cache : Std.HashMap Lean.ExprStructEq Lean.Expr),
  sizeOf { mctx := mctx, nextMacroScope := nextMacroScope, ngen := ngen, cache := cache } =
    1 + sizeOf mctx + sizeOf nextMacroScope + sizeOf ngen + sizeOf cache
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.invFun_zero : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n], MatrixEquivTensor.invFun n R A 0 = 0
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  (X : ↑(F.obj { as := Opposite.op S })),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.compIso F S).inv.app X = CategoryTheory.CategoryStruct.id S
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_mapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred]
  [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Std.Iterators.PostconditionT n γ}
  {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← (f b).run
          pure (g d c))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.mapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.toSubmodule_orthogonal_eq : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), ↑Kᗮ = (↑K)ᗮ
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_uInt16Size : ∀ (a b : Fin UInt16.size), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.continuous_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α], Continuous fun x => {x}
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- An element of `k[G]` is in the submodule generated by its support.  -/
AddMonoidAlgebra.mem_span_support_coeff : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (f : AddMonoidAlgebra k G),
  f ∈ Submodule.span k (AddMonoidAlgebra.of' k G '' ↑f.coeff.support)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instModule_1 : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) → {S : Type u_3} → [inst_2 : Semiring S] → [Module S R] → Module S (WithVal v)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.Data.Multiset.Fintype
Multiset.toEnumFinset_filter_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (a : α),
  {x ∈ m.toEnumFinset | x.1 = a} = {a} ×ˢ Finset.range (Multiset.count a m)
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.mem_leadingCoeff : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) (x : R),
  x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.zeta_mul_mu' : ∀ (𝕜 : Type u_2) (α : Type u_5) [inst : AddCommGroup 𝕜] [inst_1 : MulOneClass 𝕜] [inst_2 : PartialOrder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] [inst_5 : DecidableLE α],
  IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.mu'✝ 𝕜 = 1
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.ext : ∀ {α : Type u_1} [inst : UniformSpace α] {Y : Type u_4} [inst_1 : TopologicalSpace Y] [T2Space Y]
  {f g : UniformSpace.Completion α → Y}, Continuous f → Continuous g → (∀ (a : α), f ↑a = g ↑a) → f = g
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instPowInt64SintOfNatNat : Lean.Grind.ToInt.Pow Int64 (Lean.Grind.IntInterval.sint 64)
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.instProductive : ∀ {α : Type w} {f : α → α}, Std.Iterators.Productive (Std.Iterators.Types.RepeatIterator α f) Id
-- Mathlib.Combinatorics.Configuration
Configuration.Dual.hasPoints : (P : Type u_1) →
  (L : Type u_2) →
    [inst : Membership P L] →
      [Configuration.HasLines P L] → Configuration.HasPoints (Configuration.Dual L) (Configuration.Dual P)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_toAdditiveBialgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M] (a : AddMonoidAlgebra A (Additive M)),
  ((MonoidAlgebra.toAdditiveBialgEquiv R A M).symm a).coeff = Finsupp.mapDomain (⇑Additive.toMul) a.coeff
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_two_pow : ∀ (k : ℕ), (2 ^ k).bitIndices = [k]
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd : ℤ →
  ℤ →
    Lean.Meta.Grind.Arith.CommRing.EqCnstr →
      Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.ofIsUnitDet_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  {f : M →ₗ[R] M'} {v : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det)
  (a : M'), (LinearEquiv.ofIsUnitDet h).symm a = ((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹) a
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.OptionT.bind.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Array.Lemmas
Array.toList_inj : ∀ {α : Type u_1} {xs ys : Array α}, xs.toList = ys.toList ↔ xs = ys
-- Mathlib.Order.Concept
Concept.mem_extent_of_rel_extent : ∀ {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α},
  r' y x → x ∈ c'.extent → y ∈ c'.extent
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.nonempty_inter_support_of_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X] {s : Set X}, 0 < μ s → (s ∩ μ.support).Nonempty
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.notMem_left : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → v ∉ s
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_ofBijective : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F)
  (hf : Function.Bijective ⇑f), ⇑(RingEquiv.ofBijective f hf) = ⇑f
-- Std.Sync.CancellationToken
/-- Reasons for cancellation.
 -/
Std.CancellationReason : Type
-- Mathlib.Data.Finset.Union
Finset.image_biUnion_filter_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (s : Finset β) (g : β → α),
  ((Finset.image g s).biUnion fun a => {c ∈ s | g c = a}) = s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.ColimitCocone.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (cocone : CategoryTheory.Limits.Cocone F)
  (isColimit : CategoryTheory.Limits.IsColimit cocone) (cocone_1 : CategoryTheory.Limits.Cocone F)
  (isColimit_1 : CategoryTheory.Limits.IsColimit cocone_1),
  ({ cocone := cocone, isColimit := isColimit } = { cocone := cocone_1, isColimit := isColimit_1 }) =
    (cocone = cocone_1 ∧ isColimit ≍ isColimit_1)
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckCoalgebraFork_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.beckCoalgebraFork X).pt = X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.inter.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (m₁ m₁_1 : Std.ExtDTreeMap α β cmp),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDTreeMap α β cmp), m₂ = m₂_1 → m₁.inter m₂ = m₁_1.inter m₂_1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Reinterpret a smooth partition of unity as a continuous partition of unity.  -/
SmoothPartitionOfUnity.toPartitionOfUnity : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] → {s : Set M} → SmoothPartitionOfUnity ι I M s → PartitionOfUnity ι M s
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousWithinAt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R)
  {s : Set R} {a : R}, ContinuousWithinAt (fun x => Polynomial.eval x p) s a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_frange_of_mem : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {x : α} {f : α →₀ M}, x ∈ f.support → f x ∈ f.frange
-- Batteries.Data.Fin.Lemmas
Fin.prod_eq_prod_map_finRange : ∀ {α : Type u_1} {n : ℕ} [inst : One α] [inst_1 : Mul α] (x : Fin n → α),
  Fin.prod x = (List.map x (List.finRange n)).prod
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Whiskering a 2-square with a natural transformation at the bottom.  -/
CategoryTheory.TwoSquare.whiskerBottom : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B B' : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B → (B ⟶ B') → CategoryTheory.TwoSquare T L R B'
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.bot_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : Preorder R] (x y : X), ⊥ x y = 0
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.sum_finsetSum_index`. -/
Finsupp.sum_finset_sum_index : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N},
  (∀ (a : α), h a 0 = 0) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
-- Mathlib.Data.List.Infix
List.take_inits : ∀ {α : Type u_1} {l : List α} {n : ℕ}, (List.take n l).inits = List.take (n + 1) l.inits
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/E/K` is a tower of fields, then the spectral norm of `x : E` when regarded as an element
of the normal closure of `E` equals its spectral norm when regarding `x` as an element of `L`.  -/
spectralNorm.eq_of_normalClosure' : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  (E : IntermediateField K L) (x : ↥E),
  spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E)))
      ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) x) =
    spectralNorm K L ((algebraMap (↥E) L) x)
-- Init.Data.Int.DivMod.Bootstrap
Int.ofNat_dvd_left : ∀ {n : ℕ} {z : ℤ}, ↑n ∣ z ↔ n ∣ z.natAbs
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_eq_some_maxIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.maxIdxOn? f xs = some (List.maxIdxOn f xs h)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] (p : Polynomial R) (i i_1 : R →ₐ[S] T) (e_i : i = i_1) (x x_1 : T)
  (e_x : x = x_1) (h : Polynomial.eval₂ (↑i) x p = 0), AdjoinRoot.liftAlgHom p i x h = AdjoinRoot.liftAlgHom p i_1 x_1 ⋯
-- Init.Data.Dyadic.Basic
Dyadic.mul_one : ∀ (x : Dyadic), x * 1 = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filterMap f m) k = (Std.ExtDHashMap.Const.get? m k).bind (f k')
-- Mathlib.LinearAlgebra.Ray
/-- A multiple of a nonzero vector is in the same ray as that vector if and only if that multiple
is positive.  -/
sameRay_smul_left_iff_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M},
  v ≠ 0 → ∀ {r : R}, r ≠ 0 → (SameRay R (r • v) v ↔ 0 < r)
-- Lean.Attributes
Lean.mkAttributeImplOfConstant : Lean.Environment → Lean.Options → Lean.Name → Except String Lean.AttributeImpl
-- Mathlib.Order.Category.Preord
Preord.ofHom_apply : ∀ {X Y : Type u} [inst : Preorder X] [inst_1 : Preorder Y] (f : X →o Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (Preord.ofHom f)) x = f x
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, and `f'` is strictly monotone on the
interior, then `f` is strictly convex on `D`.
Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict monotonicity of `f'`.  -/
StrictMonoOn.strictConvexOn_of_deriv : ∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictMonoOn (deriv f) (interior D) → StrictConvexOn ℝ D f
-- Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
HomologicalComplex.isIso_π_f_of_isLimit_of_isEventuallyConstantTo : ∀ {C : Type u_1} {J : Type u_2} {ι : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} J] {c : ComplexShape ι} [CategoryTheory.IsCofiltered J]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (j : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c j))]
  {cF : CategoryTheory.Limits.Cone F} (hcF : CategoryTheory.Limits.IsLimit cF) (q : ι) (j : J),
  (F.comp (HomologicalComplex.eval C c q)).IsEventuallyConstantTo j → CategoryTheory.IsIso ((cF.π.app j).f q)
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for group homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`.  -/
AddMonoidHom.exists_range_eq_graph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddGroup I]
  {f : G →+ H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', f.range = f'.graph
-- Mathlib.CategoryTheory.Preadditive.Schur
CategoryTheory.finrank_hom_simple_simple_eq_one_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C)
  [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y],
  Module.finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.opEquiv_symm_apply : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup Mᵐᵒᵖ), (RelIso.symm Subsemigroup.opEquiv) x = x.unop
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x : αᵒᵈ}, Set.Ici (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Iic x
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.«termα⁻¹» : Lean.ParserDescr
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {i : ι}
  (p : Z.TotalSpace), ↑(Z.localTriv i) p = (p.proj, (Z.coordChange (Z.indexAt p.proj) i p.proj) p.snd)
-- Mathlib.Data.Setoid.Partition
/-- two indexes are equal if they are equal in membership  -/
IndexedPartition.eq_of_mem : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (self : IndexedPartition s) {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Y`-coordinate of a representative of `-P` for a Jacobian point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Jacobian.negY : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasEqualizer_precomp_of_equalizer : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X)
  {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s)
  {c : CategoryTheory.Limits.PullbackCone s.ι h} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.Logic.Relation
Relation.reflexive_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl (Relation.ReflTransGen r)
-- Init.Data.UInt.Bitwise
UInt16.toNat_and : ∀ (a b : UInt16), (a &&& b).toNat = a.toNat &&& b.toNat
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.iso_comm_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat)
  {Z : C} (h : (HP'.Hₚ i).obj (TopPair.ofTopCat X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (TopPair.ofTopCat X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((HP'.iso i).hom.app X)) h
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.precomposeHomEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cocone G),
  CategoryTheory.Limits.IsColimit.precomposeHomEquiv α c = CategoryTheory.Limits.IsColimit.precomposeInvEquiv α.symm c
-- Init.Data.List.Attach
List.head?_attach : ∀ {α : Type u_1} {xs : List α}, xs.attach.head? = xs.head?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The left inclusion `F.X i ⟶ (homotopyCofiber φ).X j` when `c.Rel j i`.  -/
HomologicalComplex.homotopyCofiber.inlX : {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] →
                  (i j : ι) → c.Rel j i → (F.X i ⟶ HomologicalComplex.homotopyCofiber.X φ j)
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_inv : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Inv (γ a b)]
  (x : (i : (a : α) × β a) → γ i.fst i.snd), Sigma.curry x⁻¹ = (Sigma.curry x)⁻¹
-- Aesop.Index.Basic
/-- The rule that should be applied.  -/
Aesop.IndexMatchResult.rule : {α : Type} → Aesop.IndexMatchResult α → α
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.isModule : {R : Type u} → [inst : Semiring R] → (self : SemimoduleCat R) → Module R ↑self
-- Mathlib.Data.Finset.Prod
Finset.product_image_fst : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq α],
  t.Nonempty → Finset.image Prod.fst (s ×ˢ t) = s
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_le_right : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N⁆ ≤ N
-- Lean.DocString.Markdown
/-- Registry for custom block element renderers that maps element type names to renderer names.  -/
Lean.Doc.docBlockMdExt : Lean.PersistentEnvExtension (Lean.Name × Lean.Name) (Lean.Name × Lean.Name) Lean.Doc.MdRendererState
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- An `AddSubmonoid` of an ordered additive monoid is an ordered additive monoid.  -/
AddSubmonoid.toIsOrderedAddMonoid : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] (S : AddSubmonoid M),
  IsOrderedAddMonoid ↥S
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.minD fallback ∈ t
-- Batteries.Data.List.Lemmas
List.getElem_swap_right_of_lt : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (hi : i < xs.length) (hj : j < (xs.swap i j).length), (xs.swap i j)[j] = xs[i]
-- Mathlib.Tactic.Recover
/-- auxiliary function for `getUnassignedGoalMVarDependencies`  -/
_private.Mathlib.Tactic.Recover.0.Mathlib.Tactic.getUnassignedGoalMVarDependencies.addMVars : Lean.Expr → StateRefT' IO.RealWorld (Std.HashSet Lean.MVarId) Lean.MetaM Unit
-- Mathlib.Control.ULift
ULift.instLawfulMonad_mathlib : LawfulMonad ULift.{u_2, u_1}
-- Init.Data.List.Scan.Lemmas
List.scanlM_reverse : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [inst : Monad m] {f : β → α → m β},
  List.scanlM f init as.reverse = List.reverse <$> List.scanrM (flip f) init as