mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Stopping
/-- If the indexing order has the discrete topology, then the stopped process of a strongly adapted
process is strongly adapted.  -/
MeasureTheory.StronglyAdapted.stoppedProcess_of_discrete : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : Nonempty ι] [inst_3 : LinearOrder ι]
  [inst_4 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [inst_7 : MeasurableSpace ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι} [DiscreteTopology ι],
  MeasureTheory.StronglyAdapted f u →
    MeasureTheory.IsStoppingTime f τ → MeasureTheory.StronglyAdapted f (MeasureTheory.stoppedProcess u τ)
-- Std.Data.ExtTreeMap.Lemmas
/-- Variant of `getElem!_map` that holds without `LawfulEqCmp`.  -/
Std.ExtTreeMap.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.ExtTreeMap.map f t)[k]! = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).get!
-- Mathlib.MeasureTheory.SetSemiring
/-- A semi-ring of sets `C` is a family of sets containing `∅`, stable by intersection and such that
for all `s, t ∈ C`, `s \ t` is equal to a disjoint union of finitely many sets in `C`.  -/
MeasureTheory.IsSetSemiring : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.Analysis.Normed.Ring.Basic
NormedRing.toRing : {α : Type u_5} → [self : NormedRing α] → Ring α
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.Data.Num.Lemmas
PosNum.pred_to_nat : ∀ {n : PosNum}, 1 < n → ↑n.pred = (↑n).pred
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.equivHom_apply : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (g : G),
  (TannakaDuality.FiniteGroup.equivHom k G) g =
    CategoryTheory.LaxMonoidalFunctor.isoOfComponents (TannakaDuality.FiniteGroup.equivApp g) ⋯ ⋯ ⋯
-- Init.MetaTypes
/-- The configuration for `simp`.
Passed to `simp` using, for example, the `simp +contextual` or `simp (maxSteps := 100000)` syntax.

See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`.
 -/
Lean.Meta.Simp.Config : Type
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_zero_left : ∀ {F : Type u_1} [inst : Field F] (d : ℕ), Polynomial.hilbertPoly 0 d = 0
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_empty : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.closure ∅ = ⊥
-- Init.Data.Option.Lemmas
Option.all_map : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β} {p : β → Bool},
  Option.all p (Option.map f x) = Option.all (fun a => p (f a)) x
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpEq.lt_congr_left : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y z : α},
  RBTree.RBNode.cmpEq cmp x y → (RBTree.RBNode.cmpLT cmp x z ↔ RBTree.RBNode.cmpLT cmp y z)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_δ_fst : ∀ (X Y : SSet) {n : ℕ} (i : Fin (n + 2))
  (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n + 1 })),
  ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i))
        z).1 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) z.1
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.dist.eq_1 : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (i : ι) (x_2 : E i) (j : ι) (y : E j),
  Metric.Sigma.dist ⟨i, x_2⟩ ⟨j, y⟩ = if h : i = j then dist x_2 (cast ⋯ y) else dist x_2 ⋯.some + 1 + dist ⋯.some y
-- Mathlib.Algebra.Order.Archimedean.Basic
Nonneg.instMulArchimedean : ∀ {R : Type u_3} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [Archimedean R]
  [ExistsAddOfLE R], MulArchimedean { x // 0 ≤ x }
-- Mathlib.Data.Multiset.Defs
Multiset.coe_nodup : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup ↔ l.Nodup
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁),
  ↑(AffineSubspace.map f s) = ⇑f '' ↑s
-- Mathlib.Topology.Order.HullKernel
/-- For a subset `S` of `T`, `kernel S` is the infimum of `S` (considered as a set of `α`)  -/
PrimitiveSpectrum.kernel : {α : Type u_1} → [CompleteLattice α] → {T : Set α} → Set ↑T → α
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Adjunction.mapCommMon_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_6 : F.Braided]
  [inst_7 : G.LaxBraided] [inst_8 : a.IsMonoidal],
  a.mapCommMon.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapCommMonIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapCommMonNatTrans a.unit)
        CategoryTheory.Functor.mapCommMonCompIso.hom)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {Q : Type u_4} [inst_3 : CommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃* P} (H : Submonoid.map j.toMonoidHom S = T) (x : N),
  (f.mulEquivOfMulEquiv k H) x = (f.map ⋯ k) x
-- Mathlib.Data.EReal.Inv
EReal.abs_eq_zero_iff : ∀ {x : EReal}, x.abs = 0 ↔ x = 0
-- Lean.Util.HasConstCache
Lean.HasConstCache.mk.injEq : ∀ {declNames : Array Lean.Name} (cache cache_1 : Std.HashMap.Raw Lean.Expr Bool),
  ({ cache := cache } = { cache := cache_1 }) = (cache = cache_1)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)] (x : List ((a : α) × β a)),
  Std.Internal.List.getEntry! a x =
    match x with
    | [] =>
      panicWithPosWithDecl "Std.Data.Internal.List.Associative" "Std.Internal.List.getEntry!" 67 10
        "key is not present in associative list"
    | ⟨k, v⟩ :: l => bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntry! a l
-- Mathlib.CategoryTheory.Join.Basic
/-- `mapPair` respects composition  -/
CategoryTheory.Join.mapPairComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                {J : Type u₅} →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} J] →
                    {K : Type u₆} →
                      [inst_5 : CategoryTheory.Category.{v₆, u₆} K] →
                        (Fₗ : CategoryTheory.Functor C E) →
                          (Fᵣ : CategoryTheory.Functor D E') →
                            (Gₗ : CategoryTheory.Functor E J) →
                              (Gᵣ : CategoryTheory.Functor E' K) →
                                CategoryTheory.Join.mapPair (Fₗ.comp Gₗ) (Fᵣ.comp Gᵣ) ≅
                                  (CategoryTheory.Join.mapPair Fₗ Fᵣ).comp (CategoryTheory.Join.mapPair Gₗ Gᵣ)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.torsionMulEquiv`.

---

A torsion monoid is isomorphic to its torsion submonoid.  -/
Monoid.IsTorsion.torsionMulEquiv : {G : Type u_1} → [inst : CommMonoid G] → IsMulTorsion G → ↥(CommMonoid.torsion G) ≃* G
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- A Hopf monoid is a bimonoid.  -/
CategoryTheory.Hopf.toBimon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Hopf C → CategoryTheory.Bimon C
-- Lean.Parser.Term.Basic
Lean.Parser.Term.explicitBinder.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.bitwise.eq_1 : ∀ (f : Bool → Bool → Bool) (n m : ℕ),
  Nat.bitwise f n m =
    if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := Nat.bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_isoColimit_hom_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasColimit X]
  (j : α) {Z : C} (h : CategoryTheory.Limits.colimit X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j }) h
-- Mathlib.ModelTheory.Syntax
/-- Maps a theory's symbols along a language map.  -/
FirstOrder.Language.LHom.onTheory : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → L.Theory → L'.Theory
-- Init.Data.Array.Attach
List.attachWith_mem_toArray : ∀ {α : Type u_1} {l : List α},
  l.attachWith (fun x => x ∈ l.toArray) ⋯ =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      l.attach
-- Mathlib.Algebra.Group.Defs
two_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 2 • a = a + a
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.nonneg_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a : α}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.is_nonempty : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  K.Nonempty
-- Mathlib.Algebra.EuclideanDomain.Basic
_private.Mathlib.Algebra.EuclideanDomain.Basic.0.EuclideanDomain.P : {R : Type u} → [EuclideanDomain R] → R → R → R × R × R → Prop
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_eq_of_lt`. -/
Eq.trans_lt : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a = b → b < c → a < c
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Riemann-Lebesgue lemma for functions on a real inner-product space: the integral
`∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v` tends to 0 as `w → ∞`.  -/
tendsto_integral_exp_inner_smul_cocompact : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [inst_6 : FiniteDimensional ℝ V],
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V) (nhds 0)
-- Init.Data.UInt.Bitwise
UInt32.and_lt_add_one : ∀ {b c : UInt32}, c ≠ -1 → b &&& c < c + 1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mem_support_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι}, i ∈ f.support ↔ f i ≠ 0
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.right : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α},
  (Ordnode.node s l x r).Valid → r.Valid
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If `0 : X ⟶ Y` is an epimorphism, then `Y ≅ 0`.  -/
CategoryTheory.Limits.isoZeroOfEpiZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → CategoryTheory.Epi 0 → (Y ≅ 0)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGED k fallback = t₂.getKeyGED k fallback
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Mapping from `Expr` to a variable representing it.  -/
Lean.Meta.Grind.AC.Struct.varMap : Lean.Meta.Grind.AC.Struct → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B]
  [StarHomClass F A B], NonUnitalStarRingHomClass F A B
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.norm_compLp_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g)
  (g0 : g 0 = 0) (f : ↥(MeasureTheory.Lp E p μ)), ‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instToStringStats : ToString Lean.PersistentHashMap.Stats
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.mk.inj : ∀ {R : Type u_4} {S : Type u_5} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {P : StandardEtalePair R} {x : S} {hasMap : P.HasMap x} {lift_bijective : Function.Bijective ⇑(P.lift x hasMap)}
  {P_1 : StandardEtalePair R} {x_1 : S} {hasMap_1 : P_1.HasMap x_1}
  {lift_bijective_1 : Function.Bijective ⇑(P_1.lift x_1 hasMap_1)},
  { P := P, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
      { P := P_1, x := x_1, hasMap := hasMap_1, lift_bijective := lift_bijective_1 } →
    P = P_1 ∧ x = x_1
-- Mathlib.Analysis.Convex.Body
ConvexBody.hausdorffEDist_coe : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (K L : ConvexBody V),
  Metric.hausdorffEDist ↑K ↑L = edist K L
-- Mathlib.Order.Defs.LinearOrder
le_of_not_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → b ≤ a
-- Mathlib.Data.Fin.Rev
Fin.succAbove_rev_left : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.rev.succAbove i = (p.succAbove i.rev).rev
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.eq_bot_or_isNonempty : ∀ {α : Type u_1} (H : Hypergraph α), H = ⊥ ∨ H.IsNonempty
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.ringHom_ext'_iff : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] {f g : Polynomial R →+* S},
  f = g ↔ f.comp Polynomial.C = g.comp Polynomial.C ∧ f Polynomial.X = g Polynomial.X
-- Init.Data.Nat.Basic
Nat.le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffAt.curry_right`.

---

Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffAt.along_snd : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'},
  ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y) → ContMDiffAt I' J n (fun y => f x y) y
-- Mathlib.FieldTheory.SplittingField.Construction
/-- The algebra equivalence with `SplittingFieldAux`,
which we will use to construct the field structure.  -/
Polynomial.SplittingField.algEquivSplittingFieldAux : {K : Type v} → [inst : Field K] → (f : Polynomial K) → f.SplittingField ≃ₐ[K] Polynomial.SplittingFieldAux f.natDegree f
-- Mathlib.Data.List.Triplewise
List.triplewise_singleton : ∀ {α : Type u_1} (a : α) (p : α → α → α → Prop), List.Triplewise p [a]
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddSubmonoid.LocalizationMap.AwayMap.lift_comp : ∀ {A : Type u_4} [inst : AddCommMonoid A] (x : A) {B : Type u_5} [inst_1 : AddCommMonoid B]
  (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [inst_2 : AddCommMonoid C] {g : A →+ C}
  (hg : IsAddUnit (g x)), (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg).comp ↑F = g
-- Mathlib.FieldTheory.SeparableClosure
/-- A separable extension has separable degree equal to degree.  -/
Algebra.IsSeparable.sepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Field.sepDegree F E = Module.rank F E
-- Mathlib.Analysis.Distribution.TemperedDistribution
ContinuousLinearMap.lpPairing.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (p q : ENNReal) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : p.HolderConjugate q]
  [inst_10 : NormedSpace ℝ G] [inst_11 : SMulCommClass ℝ 𝕜 G] [inst_12 : CompleteSpace G] (B B_1 : E →L[𝕜] F →L[𝕜] G),
  B = B_1 → ContinuousLinearMap.lpPairing μ p q B = ContinuousLinearMap.lpPairing μ p q B_1
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mk : {X : Type u_4} →
  [inst : TopologicalSpace X] →
    (toFun : ℕ → Set X) →
      (∀ (n : ℕ), IsCompact (toFun n)) →
        (∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1))) → ⋃ n, toFun n = Set.univ → CompactExhaustion X
-- Mathlib.Order.Hom.Basic
OrderIso.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {f g : α ≃o β}, f = g ↔ ⇑f = ⇑g
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.global.inj : ∀ {n n_1 : Lean.Name}, Lean.Widget.PanelWidgetsExtEntry.global n = Lean.Widget.PanelWidgetsExtEntry.global n_1 → n = n_1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFinset_mono : ∀ {α : Type u_1} {G : SimpleGraph α} (H : SimpleGraph α) [inst : Fintype α] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {n : ℕ} [inst_3 : DecidableRel H.Adj], G ≤ H → G.cliqueFinset n ⊆ H.cliqueFinset n
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesMonomorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.PreservesMonomorphisms ↔ G.PreservesMonomorphisms
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Swapping the first two vertices preserves similarity.  -/
Similar.comm_left : ∀ {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] {a b c : P₁}
  {a' b' c' : P₂}, Similar ![a, b, c] ![a', b', c'] → Similar ![b, a, c] ![b', a', c']
-- Mathlib.Order.Basic
Prod.instDecidableLE : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LE α] →
      [inst_1 : LE β] → {x y : α × β} → [Decidable (x.1 ≤ y.1)] → [Decidable (x.2 ≤ y.2)] → Decidable (x ≤ y)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.em : ∀ {α : Type u} (f : Ultrafilter α) (p : α → Prop), (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, ¬p x
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.range_eq_iSup : ∀ {ι : Type u_1} (G : ι → Type u_4) [inst : (i : ι) → Group (G i)] {N : Type u_5} [inst_1 : Group N]
  (f : (i : ι) → G i →* N), (Monoid.CoprodI.lift f).range = ⨆ i, (f i).range