mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Differential.Basic
/-- A finite extension of a differential field has a unique derivation which agrees with the one on the
base field.
 -/
Differential.uniqueDifferentialAlgebraFiniteDimensional : {F : Type u_2} →
  [inst : Field F] →
    [inst_1 : Differential F] →
      [CharZero F] →
        {K : Type u_3} →
          [inst_3 : Field K] →
            [inst_4 : Algebra F K] → [FiniteDimensional F K] → Unique { _a // DifferentialAlgebra F K }
-- Mathlib.Algebra.Group.ULift
ULift.sub.eq_1 : ∀ {α : Type u} [inst : Sub α], ULift.sub = { sub := fun f g => { down := f.down - g.down } }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ)
  (acc xc : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig xc curr acc).aig.decls.size
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `get?_filterMap` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.get?_filterMap' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] {f : α → β → Option γ} {k : α},
  m.WF → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filterMap f m) k = (Std.DHashMap.Raw.Const.get? m k).bind (f k)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_xor : ∀ (x y i : ℕ), (x ^^^ y).testBit i = (x.testBit i ^^ y.testBit i)
-- Mathlib.Topology.ContinuousOn
Filter.EventuallyEq.congr_continuousWithinAt_of_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, f =ᶠ[nhdsWithin x (insert x s)] g → (ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap`
map it to the same point.
 -/
CategoryTheory.Equalizer.Sieve.compatible_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (S : CategoryTheory.Sieve X) (x : CategoryTheory.Equalizer.FirstObj P S.arrows),
  CategoryTheory.Presieve.FamilyOfElements.Compatible
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.firstObjEqFamily P S.arrows).hom) x) ↔
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Sieve.firstMap P S)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Sieve.secondMap P S)) x
-- Mathlib.Algebra.Group.Submonoid.Membership
VAddAssocClass.of_mclosure_eq_top : ∀ {M : Type u_1} {N : Type u_4} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M N] [inst_2 : VAdd N α]
  [inst_3 : AddAction M α] {s : Set M},
  AddSubmonoid.closure s = ⊤ → (∀ x ∈ s, ∀ (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z) → VAddAssocClass M N α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Const.getD (Std.DHashMap.Const.insertMany m l) k fallback = Std.DHashMap.Const.getD m k fallback
-- Mathlib.Algebra.Order.Field.Basic
max_div_div_right_of_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α},
  c ≤ 0 → ∀ (a b : α), max (a / c) (b / c) = min a b / c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
fderiv_arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.arctan (f x)) x = (1 / (1 + f x ^ 2)) • fderiv ℝ f x
-- Mathlib.Algebra.Homology.Single
ChainComplex.fromSingle₀Equiv_apply : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V)
  (f : (ChainComplex.single₀ V).obj X ⟶ C), (C.fromSingle₀Equiv X) f = f.f 0
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_le_logb_of_le : ∀ {b x y : ℝ}, 1 < b → 0 < x → x ≤ y → Real.logb b x ≤ Real.logb b y
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_fin_one_of : ∀ {R : Type v} [inst : CommRing R] (a : R), !![a].det = a
-- Mathlib.Order.Bounds.Basic
Set.Nonempty.bddAbove_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.Nonempty → BddAbove (lowerBounds s)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mem_inv_pointwise_smul_iff : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S : Submonoid M} {x : M}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Algebra.Quaternion
Quaternion.ext : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b
-- Mathlib.Algebra.Homology.GrothendieckAbelian
HomologicalComplex.locallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.LocallySmall.{w, v, u} C] [Small.{w, t} ι],
  CategoryTheory.LocallySmall.{w, max t v, max (max t u) v} (HomologicalComplex C c)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyπ_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyπ (CategoryTheory.ShortComplex.leftHomologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.leftHomologyπ
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Enumerate all measures we want to try.

All measures (resp. combinations thereof) and
possible orderings of functions (if more than one)
 -/
Lean.Elab.WF.GuessLex.generateMeasures : Array ℕ → Lean.MetaM (Array Lean.Elab.WF.GuessLex.MutualMeasure)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every graph has a spanning forest.  -/
SimpleGraph.exists_isAcyclic_reachable_eq_le : ∀ {V : Type u_1} {G : SimpleGraph V}, ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.eq_1 : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (f : α → β),
  LipschitzWith K f = ∀ (x y : α), edist (f x) (f y) ≤ ↑K * edist x y
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is complex differentiable on some set `s`, then it is analytic at any point `z`
such that `s ∈ 𝓝 z` (equivalently, `z ∈ interior s`).  -/
DifferentiableOn.analyticAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E}
  {z : ℂ}, DifferentiableOn ℂ f s → s ∈ nhds z → AnalyticAt ℂ f z
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.tacticPurity_tac : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.beq : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.SplitInfo → Bool
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.mk.inj : ∀ {α : Type} {value : Option α} {pos remaining : ℕ} {value_1 : Option α} {pos_1 remaining_1 : ℕ},
  { value := value, pos := pos, remaining := remaining } =
      { value := value_1, pos := pos_1, remaining := remaining_1 } →
    value = value_1 ∧ pos = pos_1 ∧ remaining = remaining_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c)
  (x : CategoryTheory.Limits.WalkingParallelPair),
  (I.parallelPairDiagramOfIsColimit d hc).obj x = CategoryTheory.Limits.parallelPair.parallelPairObj c.pt d.pt x
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
topological groups, then we can push forward a continuous compactly supported function on `B` to a
continuous compactly supported function on `C` by integrating over `A`.  -/
TopologicalAddGroup.IsSES.pushforward : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : AddGroup A] →
          [inst_1 : AddGroup B] →
            [inst_2 : AddGroup C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →+ B} →
                      {ψ : B →+ C} →
                        TopologicalAddGroup.IsSES φ ψ →
                          [IsTopologicalAddGroup A] →
                            [IsTopologicalAddGroup B] →
                              [inst_8 : NormedAddCommGroup E] →
                                [inst_9 : MeasurableSpace A] →
                                  [BorelSpace A] →
                                    (μA : MeasureTheory.Measure A) →
                                      [hμA : μA.IsAddHaarMeasure] →
                                        [inst : NormedSpace ℝ E] →
                                          [IsTopologicalAddGroup C] →
                                            [LocallyCompactSpace B] →
                                              CompactlySupportedContinuousMap B E →ₗ[ℝ]
                                                CompactlySupportedContinuousMap C E
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsCentralScalar : ∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  [inst_2 : SMul Rᵐᵒᵖ ENNReal] [inst_3 : IsCentralScalar R ENNReal], IsCentralScalar R (MeasureTheory.OuterMeasure α)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_sub : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : SubNegZeroMonoid R] [inst_4 : ContinuousSub R] (f g : ContinuousMapZero X R), ⇑(f - g) = ⇑f - ⇑g
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertFormatPart : Std.Time.FormatPart → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap : ∀ (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] [inst_7 : Subsingleton ι] (i : ι) (f : M₂ →L[R] M₃),
  ((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i) f).toMultilinearMap =
    (MultilinearMap.ofSubsingleton R M₂ M₃ i) ↑f
-- Mathlib.Topology.GDelta.Basic
/-- A Gδ set is a countable intersection of open sets.  -/
IsGδ : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Context.mk : Lean.Name → Bool → Lean.Elab.Tactic.Context
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.ofNSMulEqZero.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) (ha : n • a = 0) (hn : n ≠ 0),
  AddUnits.ofNSMulEqZero a n ha hn = AddUnits.ofNSMul 0 a hn ha
-- Mathlib.Analysis.Complex.Basic
Complex.slitPlane_eq_union : Complex.slitPlane = {z | 0 < z.re} ∪ {z | z.im ≠ 0}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter_le_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF → ∀ {k : α} {f : Option β → Option β}, (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size ≤ (↑m).size + 1
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Sat.eq_1 : ∀ {aig : Std.Sat.AIG ℕ} (assign : ℕ → Bool) (state : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.Sat✝ assign state = Std.Sat.CNF.Sat assign (Std.Sat.AIG.toCNF.State.cnf✝ state)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_prod_of_subset_of_one_le' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s t : Finset ι}
  [MulLeftMono N], s ⊆ t → (∀ i ∈ t, i ∉ s → 1 ≤ f i) → ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.size_ofFn_go : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} {i : ℕ} {acc : Array α} {h : i ≤ n},
  (Array.ofFn.go✝ f acc i h).size = acc.size + i
-- Lean.Server.ServerTask
Lean.Server.ServerTask.bindCostly : {α : Type u_1} → {β : Type u_2} → Lean.Server.ServerTask α → (α → Lean.Server.ServerTask β) → Lean.Server.ServerTask β
-- Mathlib.Topology.Category.Compactum
/-- This definition is used to prove essential surjectivity of `compactumToCompHaus`.  -/
compactumToCompHaus.isoOfTopologicalSpace : {D : CompHaus} → compactumToCompHaus.obj (Compactum.ofTopologicalSpace ↑D.toTop) ≅ D
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer : Type
-- Lean.Parser.Term
/-- `binop% f a b` elaborates `f a b` as a binary operation using the type propagation protocol in `Lean.Elab.Extra`.  -/
Lean.Parser.Term.binop : Lean.Parser.Parser
-- Mathlib.Topology.Homotopy.Lifting
Path.map'.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ γ_1 : Path x y)
  (e_γ : γ = γ_1) {f : X → Y} (h : ContinuousOn f (Set.range ⇑γ)), γ.map' h = γ_1.map' ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {old : Std.Sat.AIG α} {w : ℕ} {aig : Std.Sat.AIG α}
  {wn wr : ℕ} {q r : aig.RefVec w} {hle : old.decls.size ≤ aig.decls.size} {aig_1 : Std.Sat.AIG α} {wn_1 wr_1 : ℕ}
  {q_1 r_1 : aig_1.RefVec w} {hle_1 : old.decls.size ≤ aig_1.decls.size},
  { aig := aig, wn := wn, wr := wr, q := q, r := r, hle := hle } =
      { aig := aig_1, wn := wn_1, wr := wr_1, q := q_1, r := r_1, hle := hle_1 } →
    aig = aig_1 ∧ wn = wn_1 ∧ wr = wr_1 ∧ q ≍ q_1 ∧ r ≍ r_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE.match_1.congr : ∀ {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α}
  {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o'),
  (∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) →
    (∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) →
      (∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) →
        (match hkky : o with
          | Ordering.gt => gt hkky
          | Ordering.eq => eq hkky
          | Ordering.lt => lt hkky) =
          match hkky : o' with
          | Ordering.gt => gt' hkky
          | Ordering.eq => eq' hkky
          | Ordering.lt => lt' hkky
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.iff_flat_and_formallyUnramified : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.Etale f ↔
    AlgebraicGeometry.Flat f ∧ AlgebraicGeometry.FormallyUnramified f ∧ AlgebraicGeometry.LocallyOfFinitePresentation f
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (φ : G ≃ₜ+ G),
  MeasureTheory.addEquivAddHaarChar φ =
    MeasureTheory.Measure.addHaar.addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) MeasureTheory.Measure.addHaar)
-- Lean.Data.PersistentHashMap
_private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.size_push : ∀ {α : Type u_1} {β : Type u_2} {ks : Array α} {vs : Array β},
  ks.size = vs.size → ∀ (k : α) (v : β), (ks.push k).size = (vs.push v).size
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_one : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) 1
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.post : Lean.Meta.Sym.Simp.Simproc
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroInt32SintOfNatNat : Lean.Grind.ToInt.Zero Int32 (Lean.Grind.IntInterval.sint 32)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.rwFixEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Lean.Log
Lean.MonadLog.toMonadFileMap : {m : Type → Type} → [self : Lean.MonadLog m] → Lean.MonadFileMap m
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then
any point has a preimage with controlled norm.  -/
ContinuousLinearMap.exists_preimage_norm_le : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E],
  Function.Surjective ⇑f → ∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {X_1 Y : X} (f : X_1 ⟶ Y),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.map f =
    ψ.right.map (S.snd.map f)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_apply_coeToLp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.setToL1 hT) ((MeasureTheory.Lp.simpleFunc.coeToLp α E ℝ) f) =
    (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.instIsLawson : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsLawson (Topology.WithLawson α)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The Lie bracket of two vectors `v` and `w` in the Lie algebra of an additive Lie
group is obtained by taking the Lie bracket of the associated invariant vector fields, at zero.  -/
instBracketAddGroupLieAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : AddGroup G] → Bracket (AddGroupLieAlgebra I G) (AddGroupLieAlgebra I G)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_def : ∀ (z : ℂ), ‖z‖ = √(Complex.normSq z)
-- Mathlib.Order.Interval.Set.Infinite
Set.Ico.infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → Infinite ↑(Set.Ico a b)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_eq_bot_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {s : AddSubmonoid M}
  {t : AddSubmonoid N}, s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.IsUniform.pos : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α}, G.IsUniform ε s t → 0 < ε
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.leftUnitor_inv_braiding_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.affineAnd_isLocal_of_propertyIsLocal : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
    (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsLocal
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.Acyclic.op : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex V c}, K.Acyclic → K.op.Acyclic
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `HahnEmbedding.Seed` extends `HahnEmbedding.ArchimedeanStrata` by specifying strictly monotone
linear maps from each `stratum` to module `R`.  -/
HahnEmbedding.Seed : (K : Type u_1) →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [IsOrderedRing K] →
        [Archimedean K] →
          (M : Type u_2) →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [IsOrderedModule K M] →
                      (R : Type u_3) → [inst_9 : AddCommGroup R] → [LinearOrder R] → [Module K R] → Type (max u_2 u_3)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_zero_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f
-- Mathlib.Data.ENat.Basic
instOrderTopENat : OrderTop ℕ∞
-- Mathlib.Topology.ContinuousMap.Algebra
/-- If an infinite product of functions in `C(α, β)` converges to `g`
(for the compact-open topology), then the pointwise product converges to `g x` for all `x ∈ α`.  -/
ContinuousMap.hasProd_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : CommMonoid β] [inst_3 : ContinuousMul β] {f : γ → C(α, β)} {g : C(α, β)} {L : SummationFilter γ},
  HasProd f g L → ∀ (x : α), HasProd (fun i => (f i) x) (g x) L
-- Init.Data.Dyadic.Basic
/-- Multiply two dyadic numbers.  -/
Dyadic.mul : Dyadic → Dyadic → Dyadic
-- Mathlib.Order.RelIso.Basic
/-- A relation homomorphism is also a relation homomorphism between dual relations.  -/
RelHom.swap : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → Function.swap r →r Function.swap s