mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_nnreal_le : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal},
  (∀ x ∈ spectrum NNReal a, f x ≤ c) → ‖cfc f a‖₊ ≤ c
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.updateBody! : Lean.IR.Decl → Lean.IR.FnBody → Lean.IR.Decl
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y X Y' X' B A : C} (i : A ⟶ B) {p : X ⟶ Y}
  {p' : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p'),
  CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i p'
-- Mathlib.Algebra.Group.Units.Basic
eq_one_of_mul_right : ∀ {α : Type u} [inst : CommMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → a = 1
-- Mathlib.Data.EReal.Basic
/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite.  -/
EReal.induction₂ : ∀ {P : EReal → EReal → Prop},
  P ⊤ ⊤ →
    (∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
      P ⊤ 0 →
        (∀ x < 0, P ⊤ ↑x) →
          P ⊤ ⊥ →
            (∀ (x : ℝ), 0 < x → P ↑x ⊤) →
              (∀ (x : ℝ), 0 < x → P ↑x ⊥) →
                P 0 ⊤ →
                  (∀ (x y : ℝ), P ↑x ↑y) →
                    P 0 ⊥ →
                      (∀ x < 0, P ↑x ⊤) →
                        (∀ x < 0, P ↑x ⊥) →
                          P ⊥ ⊤ →
                            (∀ (x : ℝ), 0 < x → P ⊥ ↑x) → P ⊥ 0 → (∀ x < 0, P ⊥ ↑x) → P ⊥ ⊥ → ∀ (x y : EReal), P x y
-- Std.Async.ContextAsync
/-- Runs a `ContextAsync` computation with a given context. See also `ContextAsync.run` for running with a new
context that automatically cancels after execution.
 -/
Std.Async.ContextAsync.runIn : {α : Type} → Std.CancellationContext → Std.Async.ContextAsync α → Std.Async.Async α
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {a₁ : ℤ × M} (a₂ : ℤ × M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval → (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval
-- Mathlib.Data.Set.Basic
Set.top_eq_univ : ∀ {α : Type u}, ⊤ = Set.univ
-- Mathlib.MeasureTheory.VectorMeasure.Prod
/-- Two vector measures `μ` and `ν` have a product with respect to `B` if there exists a
measure giving mass `B (μ s) (ν t)` to any measurable product set `s × t`.
This is satisfied whenever `μ` or `ν` has finite variation.  -/
MeasureTheory.VectorMeasure.HasProd : {X : Type u_2} →
  {Y : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          {mX : MeasurableSpace X} →
            {mY : MeasurableSpace Y} →
              [inst : NormedAddCommGroup E] →
                [inst_1 : NormedSpace ℝ E] →
                  [inst_2 : NormedAddCommGroup F] →
                    [inst_3 : NormedSpace ℝ F] →
                      [inst_4 : NormedAddCommGroup G] →
                        [inst_5 : NormedSpace ℝ G] →
                          MeasureTheory.VectorMeasure X E → MeasureTheory.VectorMeasure Y F → (E →L[ℝ] F →L[ℝ] G) → Prop
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The subfield of `K` containing all elements of `K`.  -/
Subfield.instTop : {K : Type u} → [inst : DivisionRing K] → Top (Subfield K)
-- Mathlib.Algebra.BigOperators.WithTop
/-- A product of finite terms is finite.  -/
WithBot.bot_lt_prod : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithBot M₀} [inst_4 : LT M₀], (∀ i ∈ s, ⊥ < f i) → ⊥ < ∏ i ∈ s, f i
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.toDirectLimit.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M],
  TensorProduct.toDirectLimit f M =
    TensorProduct.lift
      (Module.DirectLimit.lift R ι G f
        (fun i =>
          (TensorProduct.mk R (G i) M).compr₂
            (Module.DirectLimit.of R ι (fun _i => TensorProduct R (G _i) M)
              (fun _i _j h => LinearMap.rTensor M (f _i _j h)) i))
        ⋯)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mk.injEq : ∀ (val : Lean.Expr) (ival? : Option ℤ) (val_1 : Lean.Expr) (ival?_1 : Option ℤ),
  ({ val := val, ival? := ival? } = { val := val_1, ival? := ival?_1 }) = (val = val_1 ∧ ival? = ival?_1)
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Icc a b).Nonempty ↔ a ≤ b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.singletonSubgraph_connected : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, (G.singletonSubgraph v).Connected
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H2π_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x = 0 ↔ ↑x ∈ groupHomology.boundaries₂ A
-- Mathlib.Order.Category.CompleteLat
/-- The category of complete lattices.  -/
CompleteLat : Type (u_1 + 1)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdBornology : (p : ENNReal) → (α : Type u_4) → (β : Type u_5) → [Bornology α] → [Bornology β] → Bornology (WithLp p (α × β))
-- Mathlib.RingTheory.Conductor
/-- A technical result telling us that `(I * S) ∩ R<x> = I * R<x>` for any ideal `I` of `R`.  -/
comap_map_eq_map_adjoin_of_coprime_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R},
  Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
    Function.Injective ⇑(algebraMap (↥R[x]) S) →
      Ideal.comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥R[x]) I
-- Mathlib.Data.List.Sublists
/-- Auxiliary helper definition for `sublists'`  -/
List.sublists'Aux : {α : Type u} → α → List (List α) → List (List α) → List (List α)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instPow : {M : Type u_1} → [inst : TopologicalSpace M] → [inst_1 : Monoid M] → [ContinuousMul M] → Pow (SeparationQuotient M) ℕ
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.sub_pos_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M}, 0 < a - b ↔ b < a
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_eq`. -/
Eq.le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → a ≤ b
-- Init.Data.String.Basic
String.prev_zero : ∀ (s : String), String.Pos.Raw.prev s 0 = 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_neg : ∀ (x : ℝ), ↑(-x) = -↑x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPullback_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.functorPullback (CategoryTheory.Functor.id C) R = R
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
Polynomial.shiftedLegendre.eq_1 : ∀ (n : ℕ),
  Polynomial.shiftedLegendre n =
    ∑ k ∈ Finset.range (n + 1), Polynomial.C ((-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)) * Polynomial.X ^ k
-- Init.Data.List.Lemmas
List.getLast?_cons : ∀ {α : Type u_1} {l : List α} {a : α}, (a :: l).getLast? = some (l.getLast?.getD a)
-- Batteries.Data.Array.Merge
/-- Auxiliary definition for `mergeDedupWith`.  -/
Array.mergeDedupWith.go : {α : Type u_1} → [ord : Ord α] → Array α → Array α → (α → α → α) → Array α → ℕ → ℕ → Array α
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- A generalization of the lift `End(B/A) → End(L/K)` in an ALKB setup.
This is inverse to the restriction. See `galRestrictHom`.  -/
galLift : {A : Type u_1} →
  (K : Type u_2) →
    (L : Type u_3) →
      (L₂ : Type u_4) →
        {B : Type u_6} →
          {B₂ : Type u_7} →
            [inst : CommRing A] →
              [inst_1 : CommRing B] →
                [inst_2 : CommRing B₂] →
                  [inst_3 : Algebra A B] →
                    [inst_4 : Algebra A B₂] →
                      [inst_5 : Field K] →
                        [inst_6 : Field L] →
                          [inst_7 : Field L₂] →
                            [inst_8 : Algebra A K] →
                              [IsFractionRing A K] →
                                [inst_10 : Algebra K L] →
                                  [inst_11 : Algebra A L] →
                                    [IsScalarTower A K L] →
                                      [inst_13 : Algebra K L₂] →
                                        [inst_14 : Algebra A L₂] →
                                          [IsScalarTower A K L₂] →
                                            [inst_16 : Algebra B L] →
                                              [IsScalarTower A B L] →
                                                [IsIntegralClosure B A L] →
                                                  [inst_19 : Algebra B₂ L₂] →
                                                    [IsScalarTower A B₂ L₂] →
                                                      [Algebra.IsAlgebraic K L] → (B →ₐ[A] B₂) → L →ₐ[K] L₂
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_finite_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.coverMincard T F U n < ⊤ ↔ ∃ s, Dynamics.IsDynCoverOf T F U n ↑s ∧ ↑s.card = Dynamics.coverMincard T F U n
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : ↥(unitary A)) {t : ℝ},
  t ∈ Set.Icc 0 1 → ‖↑u - 1‖ < 2 → ‖↑(selfAdjoint.expUnitary (t • Unitary.argSelfAdjoint u)) - 1‖ ≤ ‖↑u - 1‖
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.eq_iSup_inf_genWeightSpace : ∀ (K : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : LieRing.IsNilpotent L] [inst_4 : Field K] [inst_5 : LieAlgebra K L] [inst_6 : Module K M]
  [inst_7 : LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] (N : LieSubmodule K L M),
  N = ⨆ χ, N ⊓ LieModule.genWeightSpace M ⇑χ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Y'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (i : E.I₁'),
  E.Y' i = E.Y i.snd
-- Mathlib.Order.LiminfLimsup
Filter.limsInf.eq_1 : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : Filter α), f.limsInf = sSup {a | ∀ᶠ (n : α) in f, a ≤ n}
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The Grothendieck group of an additive monoid `M` is the localization at its top submonoid.  -/
Algebra.GrothendieckAddGroup : (M : Type u_1) → [AddCommMonoid M] → Type u_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).iso = h.iso
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxKey! : {α : Type u} → {β : α → Type v} → [Inhabited α] → Std.DTreeMap.Internal.Impl α β → α
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G],
  AddSubmonoid.neg = { neg := fun S => { carrier := -↑S, add_mem' := ⋯, zero_mem' := ⋯ } }
-- Mathlib.Order.Closure
/-- The set of closed elements for `l` is the range of `u ∘ l`.  -/
LowerAdjoint.closed_eq_range_close : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u),
  l.closed = Set.range (u ∘ l.toFun)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.exists_mem_notMem_iff_ne : ∀ {α : Type u_1} {n : ℕ} (s t : ↑(Set.powersetCard α n)), s ≠ t ↔ ∃ a ∈ s, a ∉ t
-- Lean.Meta.DecLevel
Lean.Meta.DecLevelContext.mk : Bool → Lean.Meta.DecLevelContext
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`.  -/
IsLocalization.mk'_algebraMap_eq_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {A : Type u_2} {Aₛ : Type u_3} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : CommSemiring Aₛ] [inst_4 : Algebra A Aₛ] [inst_5 : Algebra R Aₛ]
  [inst_6 : IsScalarTower R A Aₛ] [inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {x : A} {s : ↥S},
  IsLocalization.mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ =
    IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The undirected angle at `p₂` between the line segments to `p₁` and
`p₃`. If either of those points equals `p₂`, this is π/2. Use
`open scoped EuclideanGeometry` to access the `∠ p₁ p₂ p₃`
notation.  -/
EuclideanGeometry.angle : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → P → P → P → ℝ
-- Mathlib.Topology.MetricSpace.Congruence
/-- Change between equivalent index sets ι and ι'.  -/
Congruent.index_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂] {E : Type u_7} [inst_2 : EquivLike E ι' ι] (f : E) (v₁ : ι → P₁) (v₂ : ι → P₂),
  Congruent (v₁ ∘ ⇑f) (v₂ ∘ ⇑f) ↔ Congruent v₁ v₂
-- Mathlib.Computability.Primrec.Basic
Primrec₂.encode_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Primrec₂ fun a b => Encodable.encode (f a b)) ↔ Primrec₂ f
-- Mathlib.Logic.Encodable.Basic
/-- Given a `Directed r` function `f : α → β` defined on an encodable inhabited type,
construct a noncomputable sequence such that `r (f (x n)) (f (x (n + 1)))`
and `r (f a) (f (x (encode a + 1))`.  -/
Directed.sequence : {α : Type u_1} →
  {β : Type u_2} → [Encodable α] → [Inhabited α] → {r : β → β → Prop} → (f : α → β) → Directed r f → ℕ → α
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_mem : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty), hs.min hn ∈ s
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr'_symm : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_eRk_sdiff_eRk_le_zero : ∀ {α : Type u_1} {M : Matroid α} {Y : Set α} (X : Set α), M.eRk Y ≤ 0 → M.eRk (X \ Y) = M.eRk X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.mk : Lean.LocalContext →
  List Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatchDiagInfo
-- Mathlib.CategoryTheory.Linear.Basic
/-- Given isomorphic objects `X ≅ Y, W ≅ Z` in a `k`-linear category, we have a `k`-linear
isomorphism between `Hom(X, W)` and `Hom(Y, Z).`  -/
CategoryTheory.Linear.homCongr : (k : Type u_1) →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : Semiring k] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear k C] → {X Y W Z : C} → (X ≅ Y) → (W ≅ Z) → (X ⟶ W) ≃ₗ[k] Y ⟶ Z
-- Mathlib.Data.Fin.SuccPred
Fin.succ_castPred_eq_add_one : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n), (a.castPred ha).succ = a + 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnostics.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.smul_negPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal),
  (r • j).negPart = r • j.negPart
-- Mathlib.Order.Heyting.Basic
sup_hnot_eq_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, a ⊔ ￢a = ⊤
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
ContinuousAlternatingMap.inCoordinates.eq_1 : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B₁ : Type u_3} (F₁ : Type u_4)
  [inst_1 : NormedAddCommGroup F₁] [inst_2 : NormedSpace 𝕜 F₁] {E₁ : B₁ → Type u_5}
  [inst_3 : (x : B₁) → AddCommGroup (E₁ x)] [inst_4 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_5 : TopologicalSpace B₁]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_7 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_8 : FiberBundle F₁ E₁] [inst_9 : VectorBundle 𝕜 F₁ E₁] {B₂ : Type u_6} (F₂ : Type u_7)
  [inst_10 : NormedAddCommGroup F₂] [inst_11 : NormedSpace 𝕜 F₂] {E₂ : B₂ → Type u_8}
  [inst_12 : (x : B₂) → AddCommGroup (E₂ x)] [inst_13 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_14 : TopologicalSpace B₂]
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_16 : (x : B₂) → TopologicalSpace (E₂ x)]
  [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] (x₀ x : B₁) (y₀ y : B₂) (ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y),
  ContinuousAlternatingMap.inCoordinates F₁ F₂ x₀ x y₀ y ϕ =
    ((Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F₂ E₂ y₀) y).compContinuousAlternatingMap
          ϕ).compContinuousLinearMap
      (Bundle.Trivialization.symmL 𝕜 (trivializationAt F₁ E₁ x₀) x)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `E / F` and `K / E` are both separable extensions, then `K / F` is also separable.  -/
Algebra.IsSeparable.trans : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E]
  [Algebra.IsSeparable E K], Algebra.IsSeparable F K
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y],
  LocallyConstant.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_subtype : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {T : ↥L} {x : X}, x ∈ L.subtype T ↔ x ∈ T
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` in the sense of strict differentiability at `f.symm a`, then `f.symm` has
the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.hasStrictFDerivAt_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F)
  {f' : E ≃L[𝕜] F} {a : F},
  a ∈ f.target → HasStrictFDerivAt (↑f) (↑f') (↑f.symm a) → HasStrictFDerivAt (↑f.symm) (↑f'.symm) a
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkAppMArgs : Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.set_add_normal_comm : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set G) (N : AddSubgroup G) [hN : N.Normal], S + ↑N = ↑N + S
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (f : CategoryTheory.Arrow C) (n : SimplexCategoryᵒᵖ),
  (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.obj n =
    CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
-- Init.Data.String.Basic
/-- Given a position in `s` that is at least `p₀`, obtain the corresponding position in
`s.sliceFrom p₀`.  -/
String.Slice.Pos.sliceFrom : {s : String.Slice} → (p₀ pos : s.Pos) → p₀ ≤ pos → (s.sliceFrom p₀).Pos
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorHom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.Center.tensorHom f g).f = CategoryTheory.MonoidalCategoryStruct.tensorHom f.f g.f
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.WEqualsLocallyBijective A] [inst_5 : CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.mk : {M : Type u_12} →
  {A : Type u_13} →
    [inst : Monoid M] →
      [inst_1 : AddMonoid A] →
        [toMulAction : MulAction M A] →
          (∀ (a : M), a • 0 = 0) → (∀ (a : M) (x y : A), a • (x + y) = a • x + a • y) → DistribMulAction M A
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.eval_separatingLeft : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], (Module.Dual.eval K V).SeparatingLeft
-- Init.Grind.Interactive
/-- Shows the pending goals.  -/
Lean.Parser.Tactic.Grind.showGoals : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMonoOn.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddRightStrictMono α], StrictMonoOn f s → ∀ (c : α), StrictMonoOn (fun x => f x + c) s
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
RingCon.mk.congr_simp : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (toCon toCon_1 : Con R) (e_toCon : toCon = toCon_1)
  (add' : ∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)),
  { toCon := toCon, add' := add' } = { toCon := toCon_1, add' := ⋯ }
-- Mathlib.Data.Fintype.EquivFin
instInfinitePerm : ∀ {α : Type u_1} [Infinite α], Infinite (Equiv.Perm α)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Ioc : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.map (Fin.castLEEmb h) (Finset.Ioc a b) = Finset.Ioc (Fin.castLE h a) (Fin.castLE h b)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.mp : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n}, T.Iff φ ψ → T.Imp φ ψ
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : { x // IsClosed x ∧ IsIrreducible x }),
  TopologicalSpace.IrreducibleCloseds.equivSubtype'.symm a = { carrier := ↑a, isIrreducible' := ⋯, isClosed' := ⋯ }
-- Mathlib.Probability.Distributions.Geometric
/-- The `positivty` tactic does not work for this goal. Use this lemma to rewrite
`(ENNReal.ofReal ((1 - p) ^ n * p)).toReal = (1 - p) ^ n * p`.  -/
ProbabilityTheory.geometricMeasure_nonneg : ∀ (p : ↑unitInterval) (n : ℕ), 0 ≤ (1 - ↑p) ^ n * ↑p