mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.Ring.of : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] →
                    [inst_6 : Nonempty ι] → (i : ι) → G i →+* DirectLimit G f
-- Mathlib.Topology.Continuous
Continuous.frontier_preimage_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (t : Set Y), frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α}, k ∈ Std.DTreeMap.Raw.ofList l cmp ↔ (List.map Sigma.fst l).contains k = true
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_edgeFinset_induce_support : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj],
  (SimpleGraph.induce G.support G).edgeFinset.card = G.edgeFinset.card
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.comp_tfst : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ α₂ β : Type u}
  (f : α₀ → F α₁) (f' : α₁ → G α₂) (x : t α₀ β),
  Functor.Comp.mk (Bitraversable.tfst f' <$> Bitraversable.tfst f x) =
    Bitraversable.tfst (Functor.Comp.mk ∘ Functor.map f' ∘ f) x
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExists.distrib_add : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g g' : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G],
  MeasureTheory.ConvolutionExists f g L μ →
    MeasureTheory.ConvolutionExists f g' L μ →
      MeasureTheory.convolution f (g + g') L μ = MeasureTheory.convolution f g L μ + MeasureTheory.convolution f g' L μ
-- Mathlib.Topology.Irreducible
/-- A preirreducible space is one where there is no non-trivial pair of disjoint opens.  -/
PreirreducibleSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g)
  [inst_2 : F.Full] [F.Faithful], CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (hf'.snd g) = h
-- Mathlib.LinearAlgebra.Span.Basic
/-- A dependent version of `submodule.iSup_induction`.  -/
Submodule.iSup_induction' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_8}
  (p : ι → Submodule R M) {motive : (x : M) → x ∈ ⨆ i, p i → Prop},
  (∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯) →
    motive 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯) →
        ∀ {x : M} (hx : x ∈ ⨆ i, p i), motive x hx
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
/-- If `C` is a monoidal closed category and `D` is a groupoid, then every functor `F : D ⥤ C` is
closed in the functor category `F : D ⥤ C` with the pointwise monoidal structure.  -/
CategoryTheory.Functor.closed : {D : Type u} →
  {C : Type u_1} →
    [inst : CategoryTheory.Groupoid D] →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] → (F : CategoryTheory.Functor D C) → CategoryTheory.Closed F
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `Polynomial.Gal.restrict p E` is compatible with `Polynomial.Gal.galAction p E`.  -/
Polynomial.Gal.restrict_smul : ∀ {F : Type u_1} [inst : Field F] {p : Polynomial F} {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits] (ϕ : Gal(E/F)) (x : ↑(p.rootSet E)),
  ↑((Polynomial.Gal.restrict p E) ϕ • x) = ϕ ↑x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.eventually_nhds_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {p : α → Prop},
  (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y
-- Mathlib.CategoryTheory.Limits.Creates
/-- If F creates the colimit of K, any cocone lifts to a colimit.  -/
CategoryTheory.liftsToColimitOfCreates : {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] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesColimit K F] →
                  (c : CategoryTheory.Limits.Cocone (K.comp F)) →
                    (t : CategoryTheory.Limits.IsColimit c) → CategoryTheory.LiftsToColimit K F c t
-- Mathlib.Analysis.Calculus.Deriv.Pi
deriv_single : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] [Finite ι] (i : ι) (y : 𝕜),
  deriv (Pi.single i) y = Pi.single i 1
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.addEquiv_symm_map_algebraMap_smul : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [inst_4 : Module S M] (r : R) (x : M),
  (RestrictScalars.addEquiv R S M).symm ((algebraMap R S) r • x) = r • (RestrictScalars.addEquiv R S M).symm x
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_int : Int.ceil = id
-- Mathlib.Analysis.Convex.Topology
/-- The convex closed hull of a set `s` is the minimal convex closed set that includes `s`.  -/
closedConvexHull : (𝕜 : Type u_2) →
  {E : Type u_3} →
    [inst : Semiring 𝕜] →
      [PartialOrder 𝕜] → [inst_2 : AddCommGroup E] → [Module 𝕜 E] → [TopologicalSpace E] → ClosureOperator (Set E)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPFunBinderTypes : Lean.Options → Bool
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
/-- Evaluating a coproduct of functors amounts to taking the coproduct of the evaluations.  -/
CategoryTheory.Limits.sigmaObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        {α : Type w} →
          [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C] →
            (f : α → CategoryTheory.Functor D C) → (d : D) → (∐ f).obj d ≅ ∐ fun s => (f s).obj d
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGED_eq_getD_getKeyGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k fallback : α},
  Std.DTreeMap.Internal.Impl.getKeyGED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGE? k t).getD fallback
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.continuousAt : ∀ {𝕜 : 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] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F], HasStrictFDerivAt f f' x → ContinuousAt f x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (lhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c lhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c_1 lhs_1) =
    (c = c_1 ∧ lhs = lhs_1)
-- Mathlib.Order.JordanHolder
CompositionSeries.snoc_eraseLast_last : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X}
  (h : JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)),
  (RelSeries.eraseLast s).snoc (RelSeries.last s) h = s
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.finsetSum : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  (s : Finset ι) {f : ι → (i : α) → E i}, (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unopFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b),
  (Bicategory.Opposite.unopFunctor a b).obj f = f.unop
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMonoid : {α : Type u} → [Semigroup α] → Monoid (WithOne α)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.card_lt_of_card_iUnion_lt : ∀ {ι α : Type u} {t : ι → Set α} {c : Cardinal.{u}}, Cardinal.mk ↑(⋃ i, t i) < c → ∀ (i : ι), Cardinal.mk ↑(t i) < c
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vadd_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] [inst_12 : TopologicalSpace V]
  [inst_13 : IsTopologicalAddTorsor P] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q),
  (f +ᵥ g).contLinear = f.contLinear + g.contLinear
-- Lean.Parser.Command
Lean.Parser.Command.attribute : Lean.Parser.Parser
-- Aesop.Search.SearchM
Aesop.SearchM.State : (Q : Type) → [Aesop.Queue Q] → Type
-- Mathlib.FieldTheory.Separable
Polynomial.eq_X_sub_C_of_separable_of_root_eq : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] {i : F →+* K} {x : F} {h : Polynomial F},
  h.Separable →
    Polynomial.eval x h = 0 →
      (Polynomial.map i h).Splits →
        (∀ y ∈ (Polynomial.map i h).roots, y = i x) → h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.max he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Data.Multiset.MapFold
Multiset.pmap_eq_map : ∀ {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
  Multiset.pmap (fun a x => f a) s H = Multiset.map f s
-- Std.Sync.Notify
Std.Notify.mk : Std.Mutex Std.Notify.State → Std.Notify
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Mathlib.Topology.Homotopy.Basic
/-- Given a `ContinuousMap.Homotopy f₀ f₁`, we can define a `ContinuousMap.Homotopy f₁ f₀` by
reversing the homotopy.
 -/
ContinuousMap.Homotopy.symm : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → f₀.Homotopy f₁ → f₁.Homotopy f₀
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_map_eval₂Hom : ∀ {R : Type u_1} {S : Type u_2} (n : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (f : R →+* S) (M : n × n → S),
  Polynomial.map (MvPolynomial.eval₂Hom f M) (Matrix.charpoly.univ R n) = (Matrix.of (Function.curry M)).charpoly
-- Init.Data.UInt.Bitwise
UInt32.not_not : ∀ {a : UInt32}, ~~~~~~a = a
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.asEmptyCone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.Limits.asEmptyCone X).pt = X
-- Init.Data.List.Nat.Sublist
List.append_left_sublist_self : ∀ {α : Type u_1} {xs : List α} (ys : List α), (xs ++ ys).Sublist ys ↔ xs = []
-- Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
/-- A bicartesian square in the lattice `Set X` gives a pushout diagram in the
category of types.  -/
CategoryTheory.Limits.Types.isPushout_of_bicartSq : ∀ {X : Type u} {S₁ S₂ S₃ S₄ : Set X} (h : Lattice.BicartSq S₁ S₂ S₃ S₄),
  CategoryTheory.IsPushout (Set.functorToTypes.map (CategoryTheory.homOfLE ⋯))
    (Set.functorToTypes.map (CategoryTheory.homOfLE ⋯)) (Set.functorToTypes.map (CategoryTheory.homOfLE ⋯))
    (Set.functorToTypes.map (CategoryTheory.homOfLE ⋯))
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
/-- Every element `x` in a unital C⋆-algebra is a linear combination of four unitary elements,
and the norm of each coefficient does not exceed `‖x‖ / 2`.  -/
CStarAlgebra.exists_sum_four_unitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : A), ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skipWhile_prop_eq_self_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  pos.skipWhile P = pos ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)
-- Batteries.Data.List.Scan
List.partialSums.eq_1 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (l : List α), l.partialSums = List.scanl (fun x1 x2 => x1 + x2) 0 l
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_createsLimitsOfSize.eq_1 : AddGrpCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.Algebra.Module.PUnit
PUnit.module : {R : Type u_1} → [inst : Semiring R] → Module R PUnit.{u_3 + 1}
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.locallyBoundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → LocallyBoundedVariationOn f s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote' ctx (Lean.Grind.CommRing.Poly.add k m p_2) =
    Lean.Grind.CommRing.Poly.denote'.go ctx p_2 (Lean.Grind.CommRing.denoteTerm ctx k m)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg),
  F.mapComp' f g fg h = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.eqToHom ⋯)) (F.mapComp f g)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_xor : ∀ {w k : ℕ} {x y : BitVec w}, BitVec.setWidth k (x ^^^ y) = BitVec.setWidth k x ^^^ BitVec.setWidth k y
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.cartan_eq_lieSpan : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H),
  H = LieSubalgebra.lieSpan R L (Set.range self.h)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_nonpos_iff : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α], |a| ≤ 0 ↔ a = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNFOfCharThree.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (W W_1 : WeierstrassCurve R),
  W = W_1 → ∀ [inst_1 : CharP R 3], W.toShortNFOfCharThree = W_1.toShortNFOfCharThree
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- This holds for all integral domains (see `Matrix.exists_mulVec_eq_zero_iff`),
not just fields, but it's easier to prove it for the field of fractions first.  -/
_private.Mathlib.LinearAlgebra.Matrix.ToLinearEquiv.0.Matrix.exists_mulVec_eq_zero_iff_aux : ∀ {n : Type u_1} [inst : Fintype n] {K : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Field K] {M : Matrix n n K},
  (∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
-- Init.Data.Vector.Lemmas
Vector.any_toList : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.toList.any p = xs.any p
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- `perm` is true if lhs and rhs are identical modulo permutation of variables.  -/
Lean.Meta.SimpTheorem.perm : Lean.Meta.SimpTheorem → Bool
-- Mathlib.Algebra.Regular.SMul
/-- An element is `M`-regular if and only if multiplying it on the left by an `M`-regular element
is `M`-regular.  -/
IsSMulRegular.smul_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [inst : SMul R M] [inst_1 : SMul R S] [inst_2 : SMul S M]
  [IsScalarTower R S M] (b : S), IsSMulRegular M a → (IsSMulRegular M (a • b) ↔ IsSMulRegular M b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ofTop_symm_apply_coe : ∀ (E : Type u_5) [inst : SeminormedAddCommGroup E] {R : Type u_12} [inst_1 : Ring R] [inst_2 : Module R E]
  (p : Submodule R E) (hp : p = ⊤) (x : E), ↑((LinearIsometryEquiv.ofTop E p hp).symm x) = x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_findGreatest : ∀ {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [inst : (x : α) → DecidablePred (p x)] {N : ℕ},
  (∀ k ≤ N, MeasurableSet {x | p x k}) → Measurable fun x => Nat.findGreatest (p x) N
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} {s : Set α}, MeasurableSet s → ρ.fst s = ρ (Prod.fst ⁻¹' s)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If an open partial homeomorphism `f` is analytic at a point `f.symm a`, with invertible
derivative, then its inverse is analytic at `a`.  -/
OpenPartialHomeomorph.analyticAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) {a : F} {i : E ≃L[𝕜] F},
  a ∈ f.target → AnalyticAt 𝕜 (↑f) (↑f.symm a) → fderiv 𝕜 (↑f) (↑f.symm a) = ↑i → AnalyticAt 𝕜 (↑f.symm) a
-- Mathlib.Topology.Maps.Strict.Group
ContinuousAddEquiv.quotientKerEquivRange.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] (hf : Topology.IsStrictMap ⇑f),
  ContinuousAddEquiv.quotientKerEquivRange hf =
    { toAddEquiv := QuotientAddGroup.quotientKerEquivRange f, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.coe_mkContinuous : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ)
  (H : ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ⇑(f.mkContinuous C H) = ⇑f
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If `s` and `t` are two fundamental domains of the same action, then their measures are equal.  -/
MeasureTheory.IsFundamentalDomain.measure_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.IsFundamentalDomain G t μ → μ s = μ t
-- Lean.Parser.Syntax
Lean.Parser.Command.macroArg : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isQuotientMap_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsQuotientMap ⇑DomMulAct.mk
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- `C` has conical limits of shape `J` if there exists a conical limit for every functor `F : J ⥤ C`.
 -/
CategoryTheory.Enriched.HasConicalLimitsOfShape : (J : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} J] →
    (V : outParam (Type u')) →
      [inst : CategoryTheory.Category.{v', u'} V] →
        [inst_1 : CategoryTheory.MonoidalCategory V] →
          (C : Type u) →
            [inst_2 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- **Gelfand-Mazur theorem**: For a complex Banach division algebra, the natural `algebraMap ℂ A`
is an algebra isomorphism whose inverse is given by selecting the (unique) element of
`spectrum ℂ a`. In addition, `algebraMap_isometry` guarantees this map is an isometry.

Note: because `NormedDivisionRing` requires the field `norm_mul : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖`, we
don't use this type class and instead opt for a `NormedRing` in which the nonzero elements are
precisely the units. This allows for the application of this isomorphism in broader contexts, e.g.,
to the quotient of a complex Banach algebra by a maximal ideal. In the case when `A` is actually a
`NormedDivisionRing`, one may fill in the argument `hA` with the lemma `isUnit_iff_ne_zero`.  -/
NormedRing.algEquivComplexOfComplete : {A : Type u_2} →
  [inst : NormedRing A] → [inst_1 : NormedAlgebra ℂ A] → [CompleteSpace A] → (∀ {a : A}, IsUnit a ↔ a ≠ 0) → ℂ ≃ₐ[ℂ] A
-- Mathlib.Order.InitialSeg
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an initial
segment embedding whose range is `Set.Iio x` for some element `x`. If `β` is a well order, this is
equivalent to the embedding not being surjective.  -/
InitialSeg.«term_≺i_» : Lean.TrailingParserDescr
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_false : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {aig : Std.Sat.AIG α} {r : α → β} {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size},
  (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.false → aig.decls[idx] = Std.Sat.AIG.Decl.false
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  (e : Z ⟶ X) (he : CategoryTheory.CategoryStruct.comp e g = 0) {Z_1 : C} (h_1 : CategoryTheory.Limits.kernel f ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g e he)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f e ⋯) h_1