mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Altitude
/-- The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the
opposite face.  -/
Affine.Simplex.altitudeFoot : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Fin (n + 1) → P
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- In a unital C⋆-algebra, if `0 ≤ a ≤ b` and `a` and `b` are units, then `b⁻¹ ≤ a⁻¹`.  -/
CStarAlgebra.inv_le_inv : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : Aˣ},
  0 ≤ ↑a → ↑a ≤ ↑b → ↑b⁻¹ ≤ ↑a⁻¹
-- Lean.Expr
/-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`.  -/
Lean.Expr.abstractRange : Lean.Expr → ℕ → Array Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.lt_card_smul_inter_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B : Finset G} {a b : G},
  ↑(B * A).card < K * ↑A.card → a ∈ B → b ∈ B → (2 - K) * ↑A.card < ↑(a • A ∩ b • A).card
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_injective_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f → Function.Injective (FirstOrder.Language.Substructure.comap f)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_smul_pos : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) {a : ℝ},
  0 ≤ a → (a • f).nnrealPart = a.toNNReal • f.nnrealPart
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_mul_eq_smul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] {r : R} {x : HahnSeries Γ R}, HahnSeries.C r * x = r • x
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element of the tree set, panicking if the set is empty.
 -/
Std.TreeSet.Raw.max! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α
-- Mathlib.Order.BooleanAlgebra.Basic
himp_le : ∀ {α : Type u} {x y z : α} [inst : BooleanAlgebra α], x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z
-- Lean.Parser.Term
Lean.Parser.Command.docComment.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide
          ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔
        w i ≤ 0
-- Mathlib.Topology.Inseparable
Specializes.snd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a b : X × Y},
  a ⤳ b → a.2 ⤳ b.2
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- See also `Ergodic.ae_empty_or_univ_of_ae_le_preimage`.  -/
Ergodic.ae_empty_or_univ_of_ae_le_preimage' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → s ≤ᵐ[μ] f ⁻¹' s → μ s ≠ ⊤ → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.symm : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {u v : V}, G'.Adj u v → G'.Adj v u
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The underlying object of `imageSubobject f` is (up to isomorphism!)
the same as the chosen object `image f`.  -/
CategoryTheory.Limits.imageSubobjectIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ≅
            CategoryTheory.Limits.image f
-- Mathlib.Computability.RE
/-- A computable predicate is one whose indicator function is computable.  -/
ComputablePred : {α : Type u_1} → [Primcodable α] → (α → Prop) → Prop
-- Lean.Data.Lsp.Diagnostics
/-- The diagnostic's code, which might appear in the user interface.  -/
Lean.Lsp.DiagnosticWith.code? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option Lean.Lsp.DiagnosticCode
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The pushout provided by `HasPushout f g` fits into an `IsPushout`.  -/
CategoryTheory.IsPushout.of_hasPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} (f : Z ⟶ X) (g : Z ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.IsPushout f g (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.range_mk : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  Set.range ArchimedeanClass.mk = Set.univ
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.directSum_R : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)), (Module.Presentation.directSum pres).R = ((i : ι) × (pres i).R)
-- Mathlib.SetTheory.ZFC.Class
Class.sInter.eq_1 : ∀ (x : Class.{u_1}), x.sInter = sInf x.classToCong
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z) (s : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f g s)
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd =
    s.snd
-- Init.Data.Array.Find
Array.findSome?_guard : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.findSome? (Option.guard p) xs = Array.find? p xs
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_empty : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.restrict ∅ = 0
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instReprIndGroupInfo.repr : Lean.Elab.Structural.IndGroupInfo → ℕ → Std.Format
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a vector and a `π / 2` rotation of that vector is zero.  -/
Orientation.inner_rotation_pi_div_two_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), inner ℝ x ((o.rotation ↑(Real.pi / 2)) x) = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' : α} {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.modify k f t) k' =
        if compare k k' = Ordering.eq then Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)
        else Std.DTreeMap.Internal.Impl.Const.get? t k'
-- Mathlib.Data.Finmap
Finmap.keys_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Finmap β), (Finmap.erase a s).keys = s.keys.erase a
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      TemperedDistribution.fourierMultiplierCLM F g₂ ∘SL TemperedDistribution.fourierMultiplierCLM F g₁ =
        TemperedDistribution.fourierMultiplierCLM F (g₁ * g₂)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
`f` grows slower than `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x, y ∈ D`,
`x < y`.  -/
Convex.image_sub_lt_mul_sub_of_deriv_lt : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, deriv f x < C) → ∀ x ∈ D, ∀ y ∈ D, x < y → f y - f x < C * (y - x)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iio_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n),
  ∏ i < Fin.castAdd m a, f i = ∏ i < a, f (Fin.castAdd m i)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.up_Rel : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α] (i j : α),
  (ComplexShape.up α).Rel i j = (i + 1 = j)
-- Aesop.Stats.File
Aesop.StatsFileRecord.toStats : Aesop.StatsFileRecord → Aesop.Stats
-- Mathlib.Order.Filter.Pointwise
Filter.top_mul_top : ∀ {α : Type u_2} [inst : Monoid α], ⊤ * ⊤ = ⊤
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_le_size_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ}, m.size ≤ (Std.DHashMap.Const.insertMany m l).size
-- Mathlib.Data.EReal.Operations
EReal.sub_self : ∀ {x : EReal}, x ≠ ⊤ → x ≠ ⊥ → x - x = 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inhabited : {R : Type u} → {M : Type v} → [Inhabited R] → [Inhabited M] → Inhabited (TrivSqZeroExt R M)
-- Mathlib.RingTheory.MvPolynomial.Tower
MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective : ∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  {x : σ → A} {p : MvPolynomial σ R},
  Function.Injective ⇑(algebraMap A B) →
    ((MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (MvPolynomial.aeval x) p = 0)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.subset.go : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.SubsetResult
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Multiplication of unit monomials.  -/
Tactic.ComputeAsymptotics.UnitMonomial.mul : Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.UnitMonomial
-- Mathlib.Analysis.Complex.Basic
Complex.isOpen_compl_range_intCast : IsOpen (Set.range Int.cast)ᶜ
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractLsb'_extractAndExtendAux : ∀ {w i k len : ℕ} {x : BitVec w} (acc : BitVec (k * len)) (hle : k ≤ w),
  (∀ i < k, BitVec.extractLsb' (i * len) len acc = BitVec.setWidth len (BitVec.extractLsb' i 1 x)) →
    BitVec.extractLsb' (i * len) len (BitVec.extractAndExtendAux k len x acc hle) =
      BitVec.setWidth len (BitVec.extractLsb' i 1 x)
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.topologicalClosure.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (s : Subgroup G),
  s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.symm : ∀ {F : Type u → Type v} [q : QPF F] (x y : (QPF.P F).W), QPF.Wequiv x y → QPF.Wequiv y x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.mk.injEq : ∀ {σ : Type} (ref : Lean.Syntax) (vars : Array Lean.Elab.Term.Do.Var) (patterns : Lean.Syntax) (rhs : σ)
  (ref_1 : Lean.Syntax) (vars_1 : Array Lean.Elab.Term.Do.Var) (patterns_1 : Lean.Syntax) (rhs_1 : σ),
  ({ ref := ref, vars := vars, patterns := patterns, rhs := rhs } =
      { ref := ref_1, vars := vars_1, patterns := patterns_1, rhs := rhs_1 }) =
    (ref = ref_1 ∧ vars = vars_1 ∧ patterns = patterns_1 ∧ rhs = rhs_1)
-- Mathlib.GroupTheory.Complement
AddSubgroup.not_isComplement_empty_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G}, ¬AddSubgroup.IsComplement S ∅
-- Mathlib.Combinatorics.Enumerative.Stirling
_private.Mathlib.Combinatorics.Enumerative.Stirling.0.Nat.stirlingFirst.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n : ℕ) → motive n.succ 0) (h_4 : (n k : ℕ) → motive n.succ k.succ),
  (match 0, 0 with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | n.succ, 0 => h_3 n
    | n.succ, k.succ => h_4 n k) =
    h_1 ()
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_star : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] [inst_5 : StarRing R] [inst_6 : ContinuousStar R]
  (f : ContinuousMapZero X R), ⇑(star f) = star ⇑f
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.getFalseProof?.go : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.quot_mk_eq_ι : ∀ (R : Type u_1) {X : Type u_2} [inst : CommSemiring R] (m : X),
  Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m) = FreeAlgebra.ι R m
-- Mathlib.Algebra.WithConv
WithConv.instDistribMulAction : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] → [inst_1 : AddCommMonoid A] → [DistribMulAction R A] → DistribMulAction R (WithConv A)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.norm_eq_iSup_rayleighQuotient : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), (↑T).IsSymmetric → ‖T‖ = ⨆ x, |T.rayleighQuotient x|
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.instMonoid : {α : Type u_1} → {mα : MeasurableSpace α} → Monoid (ProbabilityTheory.Kernel α α)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.size_eq_match_roi : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => next<...*.size + 1
-- Mathlib.GroupTheory.Torsion
CommGroup.primaryComponent.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G] (p : ℕ),
  CommGroup.primaryComponent G p = { toSubmonoid := CommMonoid.primaryComponent G p, inv_mem' := ⋯ }
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMapClass.mk : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : TopologicalSpace α] [inst_1 : Zero β]
  [inst_2 : TopologicalSpace β] [inst_3 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)) → ZeroAtInftyContinuousMapClass F α β
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.keyword.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.keyword = 1
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.baseDomain.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M),
  u.baseDomain = ⨆ c, u.stratum c
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_ext_iff : ∀ {X Y : PartOrdEmb} {f g : X ⟶ Y}, f = g ↔ PartOrdEmb.Hom.hom f = PartOrdEmb.Hom.hom g
-- Mathlib.Data.Set.Finite.Basic
Set.finite_insert : ∀ {α : Type u} {s : Set α} {a : α}, (insert a s).Finite ↔ s.Finite
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The morphisms in the category `SingleFunctors C D A`  -/
CategoryTheory.SingleFunctors.Hom : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              CategoryTheory.SingleFunctors C D A → CategoryTheory.SingleFunctors C D A → Type (max (max u_1 u_5) v_2)
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.instCommShiftLocalizedFunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {M : Type u_3} →
                [inst_2 : AddMonoid M] →
                  [inst_3 : CategoryTheory.HasShift C₁ M] →
                    [inst_4 : CategoryTheory.HasShift C₂ M] →
                      [Φ.functor.CommShift M] →
                        {D₁ : Type u_4} →
                          {D₂ : Type u_5} →
                            [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁] →
                              [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] →
                                (L₁ : CategoryTheory.Functor C₁ D₁) →
                                  [inst_8 : L₁.IsLocalization W₁] →
                                    (L₂ : CategoryTheory.Functor C₂ D₂) →
                                      [inst_9 : CategoryTheory.HasShift D₁ M] →
                                        [inst_10 : CategoryTheory.HasShift D₂ M] →
                                          [L₁.CommShift M] →
                                            [L₂.CommShift M] →
                                              [inst_13 : L₂.IsLocalization W₂] → (Φ.localizedFunctor L₁ L₂).CommShift M
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeAddMagma.liftAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : FreeAddMagma α → Sort u_2) (x : α) (h_1 : (x : α) → motive (FreeAddMagma.of x))
  (h_2 : (x y : FreeAddMagma α) → motive (x.add y)),
  (match FreeAddMagma.of x with
    | FreeAddMagma.of x => h_1 x
    | x.add y => h_2 x y) =
    h_1 x
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ofSuppBddBelow_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ] {f : Γ → R}
  {hf : BddBelow (Function.support f)}, HahnSeries.ofSuppBddBelow f hf = 0 ↔ f = 0
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mk.inj : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Ring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommGroup E}
  {inst_3 : Module 𝕜 E} {toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex E}
  {indep : ∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex.faces → AffineIndependent 𝕜 Subtype.val}
  {inter_subset_convexHull :
    ∀ {s t : Finset E},
      s ∈ toPreAbstractSimplicialComplex.faces →
        t ∈ toPreAbstractSimplicialComplex.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)}
  {toPreAbstractSimplicialComplex_1 : PreAbstractSimplicialComplex E}
  {indep_1 : ∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex_1.faces → AffineIndependent 𝕜 Subtype.val}
  {inter_subset_convexHull_1 :
    ∀ {s t : Finset E},
      s ∈ toPreAbstractSimplicialComplex_1.faces →
        t ∈ toPreAbstractSimplicialComplex_1.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)},
  { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, indep := indep,
        inter_subset_convexHull := inter_subset_convexHull } =
      { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex_1, indep := indep_1,
        inter_subset_convexHull := inter_subset_convexHull_1 } →
    toPreAbstractSimplicialComplex = toPreAbstractSimplicialComplex_1
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instAddCommSemigroup : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → AddCommSemigroup (ConvexCone R M)
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_le_card_of_injective : ∀ {α : Type u_3} {β : Type u_4} {f : α → β}, Function.Injective f → ENat.card α ≤ ENat.card β
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Init.Data.UInt.Bitwise
USize.xor_not : ∀ {a b : USize}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Lean.Elab.PreDefinition.Structural.BRecOn
Lean.Elab.Structural.searchPProd : {α : Type} → Lean.Expr → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.induction_of_closure_eq_top_right : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {motive : M → Prop},
  AddSubmonoid.closure s = ⊤ → ∀ (x : M), motive 0 → (∀ (x y : M), y ∈ s → motive x → motive (x + y)) → motive x
-- Mathlib.CategoryTheory.Square
/-- the top morphism  -/
CategoryTheory.Square.f₁₂ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Square C) → self.X₁ ⟶ self.X₂
-- Mathlib.Order.Category.PartOrd
PartOrd.of.inj : ∀ {carrier : Type u_1} {str : PartialOrder carrier} {carrier_1 : Type u_1} {str_1 : PartialOrder carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiff.comp_contMDiff : ∀ {𝕜 : 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] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F},
  ContDiff 𝕜 n g → ContMDiff I (modelWithCornersSelf 𝕜 F) n f → ContMDiff I (modelWithCornersSelf 𝕜 F') n (g ∘ f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`.  -/
AddSubmonoidClass.nsmulMemClass : ∀ {S : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : SetLike S M] [AddSubmonoidClass S M], SMulMemClass S ℕ M
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Measurability of the action of the topological group `G` on the left-coset space `G / Γ`.  -/
QuotientGroup.measurableSMul : ∀ {G : Type u_1} [inst : Group G] {Γ : Subgroup G} [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalGroup G] [BorelSpace G] [BorelSpace (G ⧸ Γ)], MeasurableSMul G (G ⧸ Γ)
-- Mathlib.GroupTheory.Abelianization.Defs
/-- The abelianization of G is the quotient of G by its commutator subgroup.  -/
Abelianization : (G : Type u) → [Group G] → Type u
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.deflate.eq_1 : ∀ {α : Type v} [small : Std.Internal.Small α] (x : α),
  Std.Internal.USquash.deflate x = { inner := Std.Internal.ComputableSmall.deflate x }
-- Mathlib.Tactic.Widget.Calc
/-- The calc widget.  -/
CalcPanel : ProofWidgets.Component CalcParams