mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.HalesJewett
/-- The word representing a combinatorial line. `l.idxfun i = none` means that
`l x i = x` for all `x` and `l.idxfun i = some y` means that `l x i = y`.  -/
Combinatorics.Line.idxFun : {α : Type u_5} → {ι : Type u_6} → Combinatorics.Line α ι → ι → Option α
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.op_inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D),
  (P.inverseImage F).op = P.op.inverseImage F.op
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory : {B : Type u_1} →
  {C : Type u_2} →
    [CategoryTheory.Bicategory C] →
      {F : B → C} → CategoryTheory.Bicategory (CategoryTheory.Bicategory.InducedBicategory C F)
-- Mathlib.Data.Finset.Image
Finset.image_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f g : α → β} {s : Finset α},
  Set.EqOn f g ↑s → Finset.image f s = Finset.image g s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `F` preserves the pushout of `f, g`, it also preserves the pushout of `g, f`.  -/
CategoryTheory.Limits.preservesPushout_symmetry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span g f) G
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.empty_carrier_carrier : ↥AlgebraicGeometry.Scheme.empty = PEmpty.{u_1 + 1}
-- Init.Data.Bool
Bool.eq_not_self_and : ∀ {a b : Bool}, a = (!a && b) ↔ (!a) = true ∧ (!b) = true
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- **Alias** of `volume_setOfPred_liouville`.

---

The set of Liouville numbers has Lebesgue measure zero.  -/
volume_setOf_liouville : MeasureTheory.volume {x | Liouville x} = 0
-- Batteries.Tactic.HelpCmd
_private.Batteries.Tactic.HelpCmd.0.Batteries.Tactic.elabHelpOption : Option Lean.Ident → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The inclusion of a summand in `∐ obj₂`.  -/
CategoryTheory.OrthogonalReflection.D₁.ιRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {Z : C} →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
          {X Y : C} → (f : X ⟶ Y) → W f → (X ⟶ Z) → (Y ⟶ ∐ CategoryTheory.OrthogonalReflection.D₁.obj₂)
-- Std.Async.Signal
/-- If:
- `s` is still running this stops `s` without resolving any remaining `AsyncTask`s that were created
  through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
  forever without further intervention.
- `s` is not yet or not anymore running this is a no-op.
 -/
Std.Async.Signal.Waiter.stop : Std.Async.Signal.Waiter → IO Unit
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.NormNoninc.id : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V], (NormedAddGroupHom.id V).NormNoninc
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {Y : C} (R : CategoryTheory.ProjectiveResolution X) (n : ℕ),
  R.extEquivCohomologyClass 0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert!_le_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insert! k v t).minKey! t.minKey!).isLE = true
-- Init.Control.Lawful.Instances
OptionT.bind_pure_comp : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] (f : α → β) (x : OptionT m α), x >>= pure ∘ f = f <$> x
-- Init.Data.List.Nat.Count
List.countP_set : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {i : ℕ} {a : α} (h : i < l.length),
  List.countP p (l.set i a) = (List.countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
-- Init.Data.UInt.Lemmas
UInt32.toFin_div : ∀ (a b : UInt32), (a / b).toFin = a.toFin / b.toFin
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_biSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) (p : ι → Prop),
  ↑(⨆ i, ⨆ (_ : p i), f i) = ⨆ i, ⨆ (_ : p i), ↑(f i)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_adj : ∀ {V : Type u_1} {W : Type u_2} {u v : V} {G : SimpleGraph W} {f : V → W},
  (SimpleGraph.comap f G).Adj u v ↔ G.Adj (f u) (f v)
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.guitartExact_iff_final : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B),
  w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.nsmul_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M), (n • f) m = n • f m
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β) (h : Monotone (↑↑f).toFun), { toMonoidHom := ↑f, monotone' := h } = f
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.symm_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  (LowerSet.map f).symm = LowerSet.map f.symm
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite product indexed by a multiset.  -/
RingCon.multisetProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : CommMonoid S] (t : RingCon S) (s : Multiset ι) {f g : ι → S},
  (∀ i ∈ s, t (f i) (g i)) → t (Multiset.map f s).prod (Multiset.map g s).prod
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castPred_self : ∀ {n : ℕ} (p : Fin (n + 1)) (h : p ≠ Fin.last n), p.succAbove (p.castPred h) = (p.castPred h).succ
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.Internal.List.extract_eq_drop_take' : ∀ {α : Type u_1} {l : List α} {start stop : ℕ}, l.extract start stop = List.drop start (List.take stop l)
-- Mathlib.RingTheory.Valuation.IsTrivialOn
Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : CommSemiring A] {B : Type u_3}
  [inst_2 : Ring B] [inst_3 : Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B),
  1 < v w → ∀ {p : Polynomial A}, p ≠ 0 → v ((Polynomial.aeval w) p) = v w ^ p.natDegree
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mem_coeffsIn_iff_coeffs_subset : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {p : MvPolynomial σ S}, p ∈ MvPolynomial.coeffsIn σ M ↔ ↑p.coeffs ⊆ ↑M
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
neg_lt_of_abs_lt : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α],
  |a| < b → -b < a
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Add β]
  [inst_3 : ContinuousAdd β], ContinuousMap.instAdd = { add := fun f g => { toFun := ⇑f + ⇑g, continuous_toFun := ⋯ } }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone.normLeOne K ↔
    x ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ NumberField.mixedEmbedding.norm x ≤ 1
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any non-trivial linearly ordered archimedean additive group is either cyclic, or densely
ordered, exclusively.  -/
LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered : ∀ {A : Type u_2} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Archimedean A] [Nontrivial A],
  IsAddCyclic A ↔ ¬DenselyOrdered A
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.one_apply : ∀ {A : Type u_2} [inst : Monoid A] [inst_1 : Star A] (a : A), 1 a = a
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ' : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1))
  (hi' : autoParam (n + i = m) SimplexCategory.δ₀Iter_σ'._auto_1),
  autoParam (↑j = ↑j' + i) SimplexCategory.δ₀Iter_σ'._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i ⋯) (SimplexCategory.σ j) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j') (SimplexCategory.δ₀Iter i hi')
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.apply.congr_simp : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F]
  [inst_9 : ContinuousSMul 𝕜 E] (m m_1 : ι → E),
  m = m_1 → ContinuousAlternatingMap.apply 𝕜 E F m = ContinuousAlternatingMap.apply 𝕜 E F m_1
-- Mathlib.Data.Fin.Tuple.Basic
/-- If a predicate `p` holds at some `x` and agrees with `q` up to that `x`, then
their `Fin.find` agree. The stronger version of `Fin.find_congr'`, since this one needs
agreement only up to `Fin.find _` while the other requires `p = q`.
Usage of this lemma will likely be via `obtain ⟨x, hx⟩ := hp; apply Fin.find_congr hx` to unify `q`,
or provide it explicitly with `rw [Fin.find_congr (q := q) hx]`.
 -/
Fin.find_congr : ∀ {n : ℕ} {p q : Fin n → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {i : Fin n} (hi : p i)
  (hpq : ∀ j ≤ i, p j ↔ q j), Fin.find p ⋯ = Fin.find q ⋯
-- Mathlib.Order.BoundedOrder.Basic
eq_top_or_lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] (a : α), a = ⊤ ∨ a < ⊤
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_sdiff_comm : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], Disjoint (x \ z) y ↔ Disjoint x (y \ z)
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Send a measure `μ` on `X` and a function `f` on `X × Y` to the function on `Y` given by
`y ↦ μ (f (·, y))`, or more suggestively, `y ↦ ∫ f(x, y) dμ(x)`.  -/
AbstractMeasure.contractFst : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] → AbstractMeasure X R R →ₗ[R] C(X × Y, R) →ₗ[R] C(Y, R)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.integrable : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y → BoxIntegral.Integrable I l f vol
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The fiber product of `L₁.X₂` and `L₀.X₃` over `L₁.X₃`. This is an auxiliary
object in the construction of the morphism `δ : L₀.X₃ ⟶ L₃.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.P : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → C
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.fst g f) =
    (TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on a closed disc of radius
`R`, then for any `w` in its interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.  -/
DifferentiableOn.circleIntegral_sub_inv_smul : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E},
  DifferentiableOn ℂ f (Metric.closedBall c R) →
    w ∈ Metric.ball c R → ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f w
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_le_of_le_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {I : Ideal R} {K : Ideal S} [inst_3 : RingHomClass F R S], I ≤ Ideal.comap f K → Ideal.map f I ≤ K
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.lowerCentralSeriesLast_le_of_not_isTrivial : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule.IsNilpotent L M],
  ¬LieModule.IsTrivial L M → LieModule.lowerCentralSeriesLast R L M ≤ LieModule.lowerCentralSeries R L M 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_dvd_prod_of_dvd : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (f g : ι → M),
  (∀ i ∈ s, f i ∣ g i) → ∏ i ∈ s, f i ∣ ∏ i ∈ s, g i
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.oproj.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7) (i_1 : ℕ)
  (var_1 : Lean.FVarId) (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7),
  (Lean.Compiler.LCNF.LetValue.oproj i var h = Lean.Compiler.LCNF.LetValue.oproj i_1 var_1 h_1) =
    (i = i_1 ∧ var = var_1)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.const : {α : Type} → Bool → Std.Tactic.BVDecide.BoolExpr α
-- Mathlib.Data.Set.Prod
Set.update_preimage_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι} [inst : DecidableEq ι] {f : (i : ι) → α i},
  (∀ (j : ι), j ≠ i → f j ∈ t j) → Function.update f i ⁻¹' Set.univ.pi t = t i
-- Mathlib.Algebra.Order.Monoid.Units
Units.val_le_val : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Preorder α] {a b : αˣ}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBot.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α α_1 : L → R),
  α = α_1 → ∀ (β β_1 : LieModule.Weight R L M), β = β_1 → LieModule.chainBot α β = LieModule.chainBot α_1 β_1
-- Mathlib.Data.List.Rotate
List.head_cyclicPermutations : ∀ {α : Type u} (l : List α), l.cyclicPermutations.head ⋯ = l
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `S` is the localization of the Jacobson ring `R` at the submonoid generated by `y : R`, then
`S` is Jacobson.  -/
isJacobsonRing_localization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
  [IsLocalization.Away y S] [H : IsJacobsonRing R], IsJacobsonRing S
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (β :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X)
  (monoidal :
    autoParam
      (∀ (U U' : C),
        (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam)
  (naturality :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β U').hom =
          CategoryTheory.CategoryStruct.comp (β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam)
  (β_1 :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X)
  (monoidal_1 :
    autoParam
      (∀ (U U' : C),
        (β_1 (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_1 U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β_1 U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam)
  (naturality_1 :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_1 U').hom =
          CategoryTheory.CategoryStruct.comp (β_1 U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam),
  ({ β := β, monoidal := monoidal, naturality := naturality } =
      { β := β_1, monoidal := monoidal_1, naturality := naturality_1 }) =
    (β = β_1)
-- Std.Data.ExtDTreeMap.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.ExtDTreeMap.foldl : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → [Std.TransCmp cmp] → (δ → (a : α) → β a → δ) → δ → Std.ExtDTreeMap α β cmp → δ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.TreeMap.unitOfList l cmp ↔ l.contains k = true
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa?!_ : Lean.ParserDescr
-- Mathlib.ModelTheory.Syntax
/-- `iExs f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by existentially
quantifying over all variables `Sum.inr _`.  -/
FirstOrder.Language.Formula.iExs : {L : FirstOrder.Language} → {α : Type u'} → (β : Type v') → [Finite β] → L.Formula (α ⊕ β) → L.Formula α
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C), HomotopicalAlgebra.WeakEquivalence X.iBifibrantResolutionObj
-- Mathlib.Data.Finset.Basic
Finset.sdiff_insert_insert_of_mem_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {x : α}, x ∈ s → x ∉ t → insert x (s \ insert x t) = s \ t
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroOneClass.toZero : {M₀ : Type u} → [self : MulZeroOneClass M₀] → Zero M₀
-- Mathlib.LinearAlgebra.LinearPMap
/-- Hypothesis for `LinearPMap.sup` holds, if `f.domain` is disjoint with `g.domain`.  -/
LinearPMap.sup_h_of_disjoint : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F),
  Disjoint f.domain g.domain → ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMapCoordChange.congr_simp : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ e₁_1 : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e_e₁ : e₁ = e₁_1)
  (e₁' e₁'_1 : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e_e₁' : e₁' = e₁'_1)
  (e₂ e₂_1 : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) (e_e₂ : e₂ = e₂_1)
  (e₂' e₂'_1 : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) (e_e₂' : e₂' = e₂'_1)
  [inst_13 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_14 : Bundle.Trivialization.IsLinear 𝕜₁ e₁']
  [inst_15 : Bundle.Trivialization.IsLinear 𝕜₂ e₂] [inst_16 : Bundle.Trivialization.IsLinear 𝕜₂ e₂'] (b b_1 : B),
  b = b_1 →
    Bundle.Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b =
      Bundle.Pretrivialization.continuousLinearMapCoordChange σ e₁_1 e₁'_1 e₂_1 e₂'_1 b_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey ⋯
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a ring homomorphism `f : α →+* β` as a monoid with zero homomorphism `α →*₀ β`.
The `simp`-normal form is `(f : α →*₀ β)`.  -/
RingHom.toMonoidWithZeroHom : {α : Type u_5} → {β : Type u_6} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ β