mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.map_add : ∀ {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.Preadditive C]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y), L.map (f₁ + f₂) = L.map f₁ + L.map f₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal - 2 * Real.pi ↔ Real.pi / 2 < θ.toReal
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filterMap f t) k =
    ((Std.ExtDTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Analysis.Distribution.Support
/-- The complement of the support is given by all *bounded* open sets on which `f` vanishes.  -/
Distribution.compl_dsupport_eq_sUnion_isBounded : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : PseudoMetricSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V},
  (Distribution.dsupport f)ᶜ = ⋃₀ {a | Distribution.IsVanishingOn f a ∧ IsOpen a ∧ Bornology.IsBounded a}
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_measureReal_iff : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  {m : MeasurableSpace β} {ν : MeasureTheory.Measure β} {t : Set β},
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_iff._auto_1 →
    autoParam (ν t ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_iff._auto_3 → (μ.real s = ν.real t ↔ μ s = ν t)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_le_beth_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c ≤ Cardinal.beth (OfNat.ofNat n) ↔ c ≤ Cardinal.beth (OfNat.ofNat n)
-- Mathlib.Data.Fintype.EquivFin
Prod.infinite_of_right : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] [Infinite β], Infinite (α × β)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).inv.hom = α.inv.app c.pt
-- Init.Prelude
/-- The homogeneous version of `HMul`: `a * b : α` where `a b : α`.  -/
Mul : Type u → Type u
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mk.inj : ∀ {k : Type u_1} {K : Type u_2} {inst : Field k} {inst_1 : Field K} {inst_2 : Algebra k K}
  {toIntermediateField : IntermediateField k K} {finiteDimensional : FiniteDimensional k ↥toIntermediateField}
  {isGalois : IsGalois k ↥toIntermediateField} {toIntermediateField_1 : IntermediateField k K}
  {finiteDimensional_1 : FiniteDimensional k ↥toIntermediateField_1} {isGalois_1 : IsGalois k ↥toIntermediateField_1},
  { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois } =
      { toIntermediateField := toIntermediateField_1, finiteDimensional := finiteDimensional_1,
        isGalois := isGalois_1 } →
    toIntermediateField = toIntermediateField_1
-- Lean.ToExpr
Lean.instToExprChar : Lean.ToExpr Char
-- Mathlib.Analysis.Convex.Intrinsic
AffineEquiv.intrinsicClosure_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V]
  [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W] [inst_7 : MetricSpace P] [inst_8 : NormedAddTorsor V P]
  [inst_9 : MetricSpace Q] [inst_10 : NormedAddTorsor W Q] (φ : P ≃ᵃ[𝕜] Q) (s : Set P),
  intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
-- Mathlib.Topology.Algebra.ConstMulAction
vadd_mem_nhds_self : ∀ {G : Type u_4} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousConstVAdd G G] {g : G} {s : Set G},
  g +ᵥ s ∈ nhds g ↔ s ∈ nhds 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If there is a single strong epi-mono factorisation of `f`, then every image factorisation is a
strong epi-mono factorisation.  -/
CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) {F' : CategoryTheory.Limits.MonoFactorisation f}
  (hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.StrongEpi F'.e
-- Mathlib.Data.Finmap
Finmap.mk : {α : Type u} → {β : α → Type v} → (entries : Multiset (Sigma β)) → entries.NodupKeys → Finmap β
-- Mathlib.Logic.Equiv.Prod
Equiv.prodAssoc_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : (α × β) × γ), (Equiv.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)
-- Mathlib.Data.PNat.Prime
PNat.Coprime.factor_eq_gcd_left_right : ∀ {a b m n : ℕ+}, m.Coprime n → a ∣ m → b ∣ n → a = m.gcd (a * b)
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.mkKey.unsafe_impl_9 : Lean.Expr → UInt64 → Lean.Meta.CanonM PUnit.{1}
-- Mathlib.Probability.Independence.Integration
/-- If a random variable `X` is independent of a sigma-algebra `m` and `A` is a set in `m`
then `∫ ω in A, f (X ω) ∂P = P.real A * ∫ ω, f (X ω) ∂P` for a measurable function `f : 𝓧 → ℝ`.  -/
ProbabilityTheory.Indep.setIntegral_eq_mul : ∀ {Ω : Type u_5} {𝓧 : Type u_6} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [m𝓧 : MeasurableSpace 𝓧]
  {X : Ω → 𝓧} {A : Set Ω},
  m ≤ mΩ →
    ∀ {f : 𝓧 → ℝ},
      ProbabilityTheory.Indep m (MeasurableSpace.comap X m𝓧) P →
        AEMeasurable X P →
          MeasurableSet A →
            MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X P) →
              ∫ (ω : Ω) in A, f (X ω) ∂P = P.real A * ∫ (ω : Ω), f (X ω) ∂P
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instConcreteCategoryMonoidHomCarrier : CategoryTheory.ConcreteCategory GrpCat fun x1 x2 => ↑x1 →* ↑x2
-- Mathlib.Order.InitialSeg
/-- Composition of two principal segment embeddings as a principal segment embedding  -/
PrincipalSeg.trans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} →
        {s : β → β → Prop} → {t : γ → γ → Prop} → [IsTrans γ t] → PrincipalSeg r s → PrincipalSeg s t → PrincipalSeg r t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.equivOfEq_trans : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E]
  {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U),
  (IntermediateField.equivOfEq hST).trans (IntermediateField.equivOfEq hTU) = IntermediateField.equivOfEq ⋯
-- Mathlib.RepresentationTheory.Rep.Res
/-- **Alias** of `Rep.resMap_hom_toLinearMap`. -/
Rep.res_map_hom_toLinearMap : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  {M N : Rep.{u_1, u, v1} k G} (p : M ⟶ N), (Rep.Hom.hom (Rep.resMap f p)).toLinearMap = (Rep.Hom.hom p).toLinearMap
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.reduce_fold_fn_preserves_induction_motive : ∀ {n : ℕ} {c_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))}
  {assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment} (idx : Fin c_arr.size)
  (res : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive c_arr assignment (↑idx) res →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive c_arr assignment (↑idx + 1)
      (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn assignment res c_arr[idx])
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) {κ' : Cardinal.{u}}
  [inst_1 : Fact κ'.IsRegular], κ ≤ κ' → (CategoryTheory.IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ')
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.modify.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : β k → β k) (size : ℕ) (k' : α)
  (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.modify k f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match h : compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.inner size k' v' (Std.DTreeMap.Internal.Impl.modify k f l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.inner size k' v' l' (Std.DTreeMap.Internal.Impl.modify k f r')
    | Ordering.eq => Std.DTreeMap.Internal.Impl.inner size k (f (cast ⋯ v')) l' r'
-- Mathlib.Topology.Algebra.Algebra
instIsSemitopologicalSemiringSubtypeMemSubalgebra : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [IsSemitopologicalSemiring A] (s : Subalgebra R A), IsSemitopologicalSemiring ↥s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  {h_contains : (m₁.diff m₂).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m₁.diff m₂) k h_contains = Std.DHashMap.Internal.Raw₀.Const.get m₁ k ⋯
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousAt.rexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {x : α},
  ContinuousAt f x → ContinuousAt (fun y => Real.exp (f y)) x
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty?.congr_simp : ∀ {ρ : Type} (pat : ρ) [self : String.Slice.Pattern.BackwardPattern pat] (s : String.Slice) (h : s.isEmpty = false),
  String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h =
    String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given an `R`-algebra `S`, the `ℤ`-linear representation associated to the natural action of
`S ≃ₐ[R] S` on `Sˣ`.  -/
Rep.ofAlgebraAutOnUnits : (R : Type u_3) →
  (S : Type u_4) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Rep.{u_4, 0, u_4} ℤ (S ≃ₐ[R] S)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n]
  [inst_6 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.mapWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let c ← (f b).run
        pure (g d c))
      init it
-- Mathlib.Topology.Baire.BaireMeasurable
/-- The preimage of a `BaireMeasurableSet` under a continuous open map is Baire measurable.  -/
BaireMeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → IsOpenMap f → ∀ {s : Set β}, BaireMeasurableSet s → BaireMeasurableSet (f ⁻¹' s)
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_ndunion : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s₁ s₂ : Multiset α),
  (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {hc : t.min! ∈ t}, t.get t.min! hc = t.min!
-- Mathlib.Analysis.Normed.Group.Hom
/-- The lifting property of the equalizer as an equivalence.  -/
NormedAddGroupHom.Equalizer.liftEquiv : {V : Type u_1} →
  {W : Type u_2} →
    {V₁ : Type u_3} →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : SeminormedAddCommGroup V₁] →
            {f g : NormedAddGroupHom V W} → { φ // f.comp φ = g.comp φ } ≃ NormedAddGroupHom V₁ ↥(f.equalizer g)
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeMonoidHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β], ⇑(FunLike.coeMonoidHom F α β) = DFunLike.coe
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α}, Filter.Tendsto f x (Filter.map f x)
-- Mathlib.Analysis.InnerProductSpace.SingularValues
/-- Connection between `LinearMap.singularValues` and `LinearMap.IsSymmetric.eigenvalues`.
Together with `LinearMap.singularValues_of_finrank_le`, this characterizes the singular values.

Because of the square root, you probably need to use
`T.isPositive_adjoint_comp_self.nonneg_eigenvalues` to make effective use of this theorem.
 -/
LinearMap.singularValues_fin : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n),
  T.singularValues ↑i = √(⋯.eigenvalues hn i)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.coeff_rename_eq_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (p : MvPowerSeries σ R) {x : τ →₀ ℕ},
  x ∉ Set.range (Finsupp.mapDomain f) → (MvPowerSeries.coeff x) ((MvPowerSeries.rename f) p) = 0
-- Mathlib.Data.Nat.Size
Nat.size_zero : Nat.size 0 = 0
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instNSMul.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  AddMonoidHom.instNSMul = { smul := fun n f => { toFun := n • ⇑f, map_zero' := ⋯, map_add' := ⋯ } }
-- Lean.Meta.Tactic.Grind.Types
/-- Performance counters  -/
Lean.Meta.Grind.State.counters : Lean.Meta.Grind.State → Lean.Meta.Grind.Counters
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurve.comp_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v → ∀ (a : ℝ), IsMIntegralCurve (γ ∘ fun x => x * a) (a • v)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is differentiable.  -/
MDifferentiable.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)}, MDiff (T% ϕ) → MDiff (T% v) → MDiff fun m => ⟨b m, (ϕ m) (v m)⟩
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_mul_self : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsStarNormal a) CFC.abs_mul_self._auto_1 → CFC.abs (a * a) = star a * a
-- Init.Data.UInt.Basic
/-- Bitwise left shift for 32-bit unsigned integers. Usually accessed via the `<<<` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.shiftLeft : UInt32 → UInt32 → UInt32
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.addLeftMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)], AddLeftMono (Lex (Π₀ (i : ι), α i))
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mkₐ_toRingHom : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), ↑(AdjoinRoot.mkₐ f) = AdjoinRoot.mk f
-- Mathlib.Algebra.Group.AddChar
AddChar.compAddMonoidHom_injective_right : ∀ {A : Type u_1} {B : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : Monoid M]
  (ψ : AddChar B M), Function.Injective ⇑ψ → Function.Injective fun f => ψ.compAddMonoidHom f
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.ofList : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List ((a : α) × β a) → Std.DHashMap α β
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.isLocallyDirected_of_equifibered_of_injective : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] {F G : CategoryTheory.Functor J AlgebraicGeometry.Scheme}
  (s : F ⟶ G) [Quiver.IsThin J],
  CategoryTheory.NatTrans.Equifibered s →
    (∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)) →
      ∀ [(G.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected],
        (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_ball_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'],
  SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is connected, any functor to a discrete category is constant on objects.
The converse is given in `IsConnected.of_any_functor_const_on_obj`.
 -/
CategoryTheory.any_functor_const_on_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂}
  (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j'
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.toSheafify.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  J.toSheafify P = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap (J.toPlus P))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.revlex.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Power),
  p₁.revlex p₂ = (p₁.x.revlex p₂.x).then (Lean.Grind.CommRing.powerRevlex p₁.k p₂.k)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Iio : ∀ {n : ℕ} (i : Fin n), Finset.map Fin.castSuccEmb (Finset.Iio i) = Finset.Iio i.castSucc
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.toFun_eq_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] (φ : R →* S) (A : Type v) (B : Type w)
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), f.toFun = ⇑f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.minKeyD fallback = fallback
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.map_surjective_of_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : SMulCommClass S A B],
  Function.Surjective ⇑(algebraMap A B) → Function.Surjective ⇑(KaehlerDifferential.map R S A B)
-- Mathlib.Analysis.Convex.Approximation
/-- Let `φ : E → ℝ` be a convex and lower-semicontinuous function on a closed convex subset `s`. For
any point `x ∈ s` and `a < φ x`, there exists a continuous affine linear function `f` in `E` such
that `f ≤ φ` on `s` and `f x = a`. This is an auxiliary lemma used in the proof of
`ConvexOn.sSup_affine_eq.`  -/
ConvexOn.exists_affine_le_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {x : E} {a : ℝ},
  x ∈ s →
    a < φ x →
      IsClosed s →
        LowerSemicontinuousOn φ s →
          ConvexOn ℝ s φ →
            ∃ l c, s.domRestrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c ≤ s.domRestrict φ ∧ RCLike.re (l x) + c = a
-- Mathlib.Order.Lattice
ite_le_sup : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α) (P : Prop) [inst_1 : Decidable P], (if P then a else b) ≤ a ⊔ b
-- Mathlib.Analysis.InnerProductSpace.TwoDim
_private.Mathlib.Analysis.InnerProductSpace.TwoDim.0.Orientation.termJ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_smul_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (s : ι → Set α) (t : Set β),
  (⋂ i, s i) • t ⊆ ⋂ i, s i • t