mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.add_sub_cancel : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] {a b : M}, a + b - b = a
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.toElementaryEmbedding.toEmbedding = f.toEmbedding
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.mk.inj : ∀ {carrier : Type u} {str : AddCommGroup carrier} {carrier_1 : Type u} {str_1 : AddCommGroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Init.Data.Option.Lemmas
Option.all_filter : ∀ {α : Type u_1} {p q : α → Bool} (o : Option α), Option.all q (Option.filter p o) = Option.all (fun a => !p a || q a) o
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.ext : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {f g : TestFunction Ω F n},
  (∀ (a : E), f a = g a) → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.mk.sizeOf_spec : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (simplex : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 }))
  (d₂ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 2 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₁.edge)
      SSet.Truncated.Edge.CompStruct.d₂._autoParam)
  (d₀ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₁₂.edge)
      SSet.Truncated.Edge.CompStruct.d₀._autoParam)
  (d₁ :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
          simplex =
        e₀₂.edge)
      SSet.Truncated.Edge.CompStruct.d₁._autoParam),
  sizeOf { simplex := simplex, d₂ := d₂, d₀ := d₀, d₁ := d₁ } = 1 + sizeOf simplex + sizeOf d₂ + sizeOf d₀ + sizeOf d₁
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.eLpNorm'_trim : ∀ {α : Type u_1} {ε : Type u_3} {m m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.eLpNorm' f q (μ.trim hm) = MeasureTheory.eLpNorm' f q μ
-- Std.Time.Date.Unit.Week
Std.Time.Week.instSubOffset : Sub Std.Time.Week.Offset
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- One of the components of the iterated derivative of a continuous multilinear map. Given a
bijection `e` between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a
continuous multilinear map of `k` vectors `v₁, ..., vₖ`, mapping them
to `f (x₁, (v_{e.symm 2})₂, x₃, ...)`, where at indices `i` in `s` one uses the `i`-th coordinate of
the vector `v_{e.symm i}` and otherwise one uses the `i`-th coordinate of a reference vector `x`.
This is continuous multilinear in the components of `x` outside of `s`, and in the `v_j`.  -/
ContinuousMultilinearMap.iteratedFDerivComponent : {𝕜 : Type u} →
  {ι : Type v} →
    {E₁ : ι → Type wE₁} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [Fintype ι] →
                    {α : Type u_1} →
                      [Fintype α] →
                        ContinuousMultilinearMap 𝕜 E₁ G →
                          {s : Set ι} →
                            α ≃ ↑s →
                              [DecidablePred fun x => x ∈ s] →
                                ContinuousMultilinearMap 𝕜 (fun i => E₁ ↑i)
                                  (ContinuousMultilinearMap 𝕜 (fun x => (i : ι) → E₁ i) G)
-- Mathlib.RepresentationTheory.Basic
/-- Turns a `CommGroup` `G` with a `MulDistribMulAction` of a monoid `M` into a
`ℤ`-linear `M`-representation on `Additive G`.  -/
Representation.ofMulDistribMulAction : (M : Type u_1) →
  (G : Type u_2) →
    [inst : Monoid M] → [inst_1 : CommGroup G] → [MulDistribMulAction M G] → Representation ℤ M (Additive G)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The initial configuration.  -/
Turing.TM0.init : {Γ : Type u_1} → {Λ : Type u_2} → [Inhabited Λ] → [inst : Inhabited Γ] → List Γ → Turing.TM0.Cfg Γ Λ
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_order_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} (n : ℕ), n • f.order ≤ (f ^ n).order
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHomClass.toMulHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : MulOne M} {inst_1 : MulOne N}
  {inst_2 : FunLike F M N} [self : MonoidHomClass F M N], MulHomClass F M N
-- Mathlib.Algebra.Ring.Defs
Ring.toAddGroupWithOne : {R : Type u} → [self : Ring R] → AddGroupWithOne R
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderOrdOpposite : ∀ {α : Type u_1} {il : LE α} {io : Ord α} [Std.LawfulOrderOrd α], Std.LawfulOrderOrd α
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instCompleteLattice : (M : Type u_1) → [inst : MulOneClass M] → CompleteLattice (SaturatedSubmonoid M)
-- Mathlib.Data.Vector.Basic
List.Vector.insertIdx_val : ∀ {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : List.Vector α n},
  ↑(List.Vector.insertIdx a i v) = (↑v).insertIdx (↑i) a
-- Std.Sync.Notify
/-- Create a new notify.
 -/
Std.Notify.new : BaseIO Std.Notify
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_subset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion ⊆ ↑I
-- Mathlib.Topology.Connected.Clopen
isClopen_iff : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : Set α}, IsClopen s ↔ s = ∅ ∨ s = Set.univ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.i =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- The remainder upon division by `of' k G g`.  -/
AddMonoidAlgebra.modOf : {k : Type u_1} →
  {G : Type u_2} → [inst : Semiring k] → [AddCommMonoid G] → AddMonoidAlgebra k G → G → AddMonoidAlgebra k G
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
ContinuousLinearMap.hasFDerivWithinAt_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F}
  {x : G'} {s : Set G'},
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      HasFDerivWithinAt (fun y => (B (f y)) (g y))
        (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) s x
-- Mathlib.Order.Prod.Lex.Hom
Prod.Lex.toLexOrderHom_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] (a : α × β),
  Prod.Lex.toLexOrderHom a = toLex a
-- Init.Data.Int.DivMod.Pow
_private.Init.Data.Int.DivMod.Pow.0.Int.fdiv_pow : ∀ {a b : ℤ} {n : ℕ}, b ∣ a → a.fdiv b ^ n = (a ^ n).fdiv (b ^ n)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.mk : ∀ {R : Type u_1} [inst : TopologicalSpace R] {A : Type u_2} [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A], τA = moduleTopology R A → IsModuleTopology R A
-- Init.Grind.AC
Lean.Grind.AC.Seq.startsWithVar_k_var : ∀ (y x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var y).startsWithVar_k x = (x == y)
-- Qq.Macro
/-- `Q(α)` is the type of Lean expressions having type `α`.   -/
Qq.«termQ(__)_1» : Lean.ParserDescr
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_sub_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree g) < m.toSyn (m.degree f) → m.leadingCoeff (f - g) = m.leadingCoeff f
-- Mathlib.MeasureTheory.Group.Integral
/-- If some right-translate of a function negates it, then the integral of the function with
respect to a right-invariant measure is 0.  -/
MeasureTheory.integral_eq_zero_of_add_right_eq_neg : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} {f : G → E} {g : G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddRightInvariant],
  (∀ (x : G), f (x + g) = -f x) → ∫ (x : G), f x ∂μ = 0
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_eq : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G →+ G'},
  Function.Surjective ⇑f → f.ker ≤ H → (AddSubgroup.map f H).index = H.index
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_prime : ∀ {p : ℕ}, Nat.Prime p → p.primeFactorsList = [p]
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mk : {α : Type u_6} →
  (sets : Set (Set α)) → sets.Nonempty → (∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) → FilterBasis α
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.zero_mem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), 0 ∈ N
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.affineCombination_eq_touchpoint_iff : ∀ {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 : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))}
  {i : Fin (n + 1)} {w : Fin (n + 1) → ℝ},
  ∑ j, w j = 1 →
    ((Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i ↔ w = s.touchpointWeights signs i)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.aut : {S : Type u_1} →
  {R : Type u_2} → [inst : Mul R] → [inst_1 : Add R] → [inst_2 : Star R] → [inst_3 : SMul S R] → Group (R ≃⋆ₐ[S] R)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF_zero_var : ∀ (μ : ℝ), ProbabilityTheory.gaussianPDF μ 0 = 0
-- Mathlib.Analysis.Normed.Ring.Units
/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹` is `O(t ^ 2)` as `t → 0`.  -/
NormedRing.inverse_add_norm_diff_second_order : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  (fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[nhds 0] fun t => ‖t‖ ^ 2
-- Mathlib.GroupTheory.PGroup
/-- A group of order `p ^ 2` is commutative. See also `IsPGroup.commutative_of_card_eq_prime_sq`
for just the proof that `∀ a b, a * b = b * a`  -/
IsPGroup.commGroupOfCardEqPrimeSq : {p : ℕ} → {G : Type u_1} → [Group G] → [Fact (Nat.Prime p)] → Nat.card G = p ^ 2 → CommGroup G
-- Std.Data.DTreeMap.Raw.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.DTreeMap.Raw.any : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ((a : α) → β a → Bool) → Bool
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.instIterator : {m : Type w → Type w'} →
  {β α₁ α₂ : Type w} →
    [Monad m] → [Std.Iterator α₁ m β] → [Std.Iterator α₂ m β] → Std.Iterator (Std.Iterators.Types.Append α₁ α₂ m β) m β
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_eq_csSup : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [inst_6 : CStarModule A E] [StarOrderedRing A] (v : E),
  ‖v‖ = sSup {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖inner A w v‖ = x}
-- Mathlib.Topology.EMetricSpace.Defs
ULift.edist_up_up : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : α), edist { down := x } { down := y } = edist x y
-- Mathlib.Geometry.Manifold.SmoothApprox
Continuous.exists_contMDiff_approx : ∀ {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {f : M → F} {ε : M → ℝ} (n : ℕ∞),
  Continuous f →
    Continuous ε →
      (∀ (x : M), 0 < ε x) → ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ Function.support ⇑g ⊆ Function.support f
-- Mathlib.Data.ENNReal.Operations
ENNReal.sSup_add : ∀ {s : Set ENNReal} {a : ENNReal}, s.Nonempty → sSup s + a = ⨆ b ∈ s, b + a
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.inside.injEq : ∀ (delta delta_1 : ℕ),
  (Lean.Server.Completion.HoverInfo.inside delta = Lean.Server.Completion.HoverInfo.inside delta_1) = (delta = delta_1)
-- Mathlib.RepresentationTheory.Intertwining
/-- The backward map of an equivalence.

Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead.  -/
Representation.Equiv.invFun : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] → {ρ : Representation A G V} → {σ : Representation A G W} → ρ.Equiv σ → W → V
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- **Alias** of `AddSubmonoidClass.coe_finsetSum`. -/
AddSubmonoidClass.coe_finset_sum : ∀ {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : SetLike B M]
  [inst_2 : AddSubmonoidClass B M] (f : ι → ↥S) (s : Finset ι), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h : t.WF) {k : α} {f : β k → β k} {hc : k ∈ t.modify k f},
  (t.modify k f).get k hc = f (t.get k ⋯)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Map a TM statement across a function. This does nothing to move statements and maps the write
values.  -/
Turing.TM0.Stmt.map : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {Γ' : Type u_2} → [inst_1 : Inhabited Γ'] → Turing.PointedMap Γ Γ' → Turing.TM0.Stmt Γ → Turing.TM0.Stmt Γ'
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `𝟙 _ ◁ η`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftId : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m] →
    Mathlib.Tactic.BicategoryLike.NormalExpr →
      Mathlib.Tactic.BicategoryLike.NormalExpr →
        Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Order.WithBot
WithBot.lt_unbotA_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithBot α} [inst_1 : Nonempty α], x ≠ ⊥ → (a < x.unbotA ↔ ↑a < x)
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear.eq_2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mem_of_self : ∀ {α : Type u_1} {m : α}, m ∈ FreeMonoid.of m
-- Mathlib.Order.Filter.Cocardinal
Filter.cocardinal_inf_principal_neBot_iff : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α},
  (Filter.cocardinal α hreg ⊓ Filter.principal s).NeBot ↔ c ≤ Cardinal.mk ↑s
-- Mathlib.Algebra.Order.Module.Synonym
Lex.instModule' : {α : Type u_1} → {β : Type u_2} → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [Module α β] → Module α (Lex β)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_of_terminates : ∀ {α : Type u} {s : Stream'.Seq α} (h : s.Terminates), s.length' = ↑(s.length h)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsClique.even_iff_exists_isMatching : ∀ {V : Type u_1} {G : SimpleGraph V} {u : Set V},
  G.IsClique u → u.Finite → (Even u.ncard ↔ ∃ M, M.verts = u ∧ M.IsMatching)
-- Mathlib.Topology.Compactness.Lindelof
Set.Finite.isLindelof_biUnion : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
  s.Finite → (∀ i ∈ s, IsLindelof (f i)) → IsLindelof (⋃ i ∈ s, f i)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- To check a linear map preserves multiplication, it suffices to check it on pure tensors. See
`algHomOfLinearMapTensorProduct` for a bundled version.  -/
LinearMap.map_mul_of_map_mul_tmul : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] {f : TensorProduct R A B →ₗ[S] C},
  (∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) →
    ∀ (x y : TensorProduct R A B), f (x * y) = f x * f y
-- Mathlib.Analysis.Normed.Ring.Basic
/-- If `α` is a seminormed ring with `‖1‖₊ = 1`, then `‖a ^ n‖₊ ≤ ‖a‖₊ ^ n`.
See also `nnnorm_pow_le'`.  -/
nnnorm_pow_le : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] (a : α) (n : ℕ), ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
-- Lean.Server.References
/-- Whether the `all` flag is set on this import.  -/
Lean.Server.ModuleImport.isAll : Lean.Server.ModuleImport → Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.Icc_union_Icc_angleDiff_add_arg : ∀ {x y : Circle},
  x ≠ y →
    Set.Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Icc (↑y).arg (y.angleDiff x + (↑y).arg) =
      Set.Icc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.of_surjective`.

---

The image of a surjective torsion additive group homomorphism is torsion.  -/
AddIsTorsion.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H},
  Function.Surjective ⇑f → IsAddTorsion G → IsAddTorsion H
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_attach_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N},
  ∑ x ∈ s.attach, h (↑x) (f ↑x) = ∑ x ∈ s, h x (f x)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_nnratCast : ∀ (q : ℚ≥0), ‖↑q‖ = ↑q
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_injective : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ}, Function.Injective Finsupp.embSigma
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.instIsReduced : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [IsReduced R], IsReduced (MvPolynomial σ R)
-- Mathlib.GroupTheory.CoprodI
/-- The **Ping-Pong-Lemma**.

Given a group action of `G` on `X` so that the `H i` acts in a specific way on disjoint subsets
`X i` we can prove that `lift f` is injective, and thus the image of `lift f` is isomorphic to the
free product of the `H i`.

Often the Ping-Pong-Lemma is stated with regard to subgroups `H i` that generate the whole group;
we generalize to arbitrary group homomorphisms `f i : H i →* G` and do not require the group to be
generated by the images.

Usually the Ping-Pong-Lemma requires that one group `H i` has at least three elements. This
condition is only needed if `# ι = 2`, and we accept `3 ≤ # ι` as an alternative.
 -/
Monoid.CoprodI.lift_injective_of_ping_pong : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G),
  (3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
    ∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
      (∀ (i : ι), (X i).Nonempty) →
        Pairwise (Function.onFun Disjoint X) →
          (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
            ∀ [Nontrivial ι], Function.Injective ⇑(Monoid.CoprodI.lift f)
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instDecidableEqOrderRel.decEq : {a : ℕ} → (x x_1 : FirstOrder.Language.orderRel a) → Decidable (x = x_1)
-- Init.GrindInstances.ToInt
Lean.Grind.ofNat_FinZero : ∀ (n : ℕ) [inst : NeZero n], ↑(OfNat.ofNat 0) = 0
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A local frame locally spans the space of sections for `V`: for each local frame `s i` on an open
set `u` around `x`, we have `t = ∑ i, hs.coeff i x (t x) • (s i x)` near `x`.  -/
IsLocalFrameOn.eventually_eq_sum_coeff_smul : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} [inst_13 : Fintype ι] (hs : IsLocalFrameOn I F n s u) (t : (x : M) → V x),
  u ∈ nhds x → ∀ᶠ (x' : M) in nhds x, t x' = ∑ i, (hs.coeff i x') (t x') • s i x'
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.mk : Lean.MetavarContext →
  Array Lean.Name → ℕ → Std.HashMap Lean.ExprStructEq Lean.Expr → Lean.MetavarContext.LevelMVarToParam.State
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendIsometry_toHomeomorph : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ), (Fin.appendIsometry m n).toHomeomorph = Fin.appendHomeomorph m n
-- Mathlib.Topology.Path
Path.target : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ 1 = y
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_mk : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (toFun : α → HahnSeries Γ R) (h1 : (⋃ a, (toFun a).support).IsPWO)
  (h2 : ∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite),
  ⇑{ toFun := toFun, isPWO_iUnion_support' := h1, finite_co_support' := h2 } = toFun