mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Builder.NormSimp
Aesop.RuleBuilder.simpCore : Lean.Name → Aesop.PhaseSpec → Lean.MetaM Aesop.LocalRuleSetMember
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.mapL_comp_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] {A : Type u_6} [inst_9 : NormedAddCommGroup A]
  [inst_10 : InnerProductSpace 𝕜 A] (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) (g : G →L[𝕜] H),
  TensorProduct.mapL f₁ g ∘SL ContinuousLinearMap.rTensor G f₂ = TensorProduct.mapL (f₁ ∘SL f₂) g
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.html : ProofWidgets.ExprPresentationData → ProofWidgets.Html
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_empty : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G)
  {U : Set G}, MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ⊥ = 0
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.algebraMap_apply' : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (r : R),
  (algebraMap R (TensorProduct R A B)) r = 1 ⊗ₜ[R] (algebraMap R B) r
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddCommGroupQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddCommGroup M] → (c : ModuleCon S M) → AddCommGroup (ModuleCon.Quotient M c)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_abs : ∀ {w i : ℕ} {x : BitVec w} (h : i < w), x.abs[i] = if x.msb = true then (-x)[i] else x[i]
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.center_eq_top : ∀ (R : Type u) [inst : CommSemiring R] (A : Type u_1) [inst_1 : StarRing R] [inst_2 : NonUnitalCommSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], NonUnitalStarSubalgebra.center R A = ⊤
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `M` be a smooth σ-compact manifold with a metric. Let `K : ι → Set M` be a locally finite
family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for all
`i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and `x ∈ K i`,
we have `Metric.closedBall x (δ x) ⊆ U i`.  -/
Metric.exists_contMDiffMap_forall_closedBall_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] {n : ℕ∞} {M : Type u_1}
  [inst_4 : MetricSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] {K U : ι → Set M},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : sInfHom α β)
  (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)), ⇑{ tosInfHom := f, map_sSup' := hf } = ⇑f
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.mem_closure_iff_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α}, M.IsColoop e → (e ∈ M.closure X ↔ e ∈ X)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.id_tensorHom_id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X₁ X₂ : CategoryTheory.LocalizedMonoidal L W ε),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
      (CategoryTheory.CategoryStruct.id X₂) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
-- Lean.Parser.Term
Lean.Parser.Term.generalizingParam.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.top_toAddSubgroup : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], ⊤.toAddSubgroup = ⊤
-- Mathlib.Data.Set.Prod
/-- **Alias** of the reverse direction of `Set.graphOn_nonempty`. -/
Set.Nonempty.graphOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, s.Nonempty → (Set.graphOn f s).Nonempty
-- Init.Data.Vector.Lemmas
Vector.flatten_push : ∀ {α : Type u_1} {n m : ℕ} {xss : Vector (Vector α n) m} {xs : Vector α n},
  (xss.push xs).flatten = Vector.cast ⋯ (xss.flatten ++ xs)
-- Mathlib.Order.Concept
/-- **Alias** of `Concept.intent_max`. -/
Concept.intent_sup : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r), (c ⊔ d).intent = c.intent ∩ d.intent
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited Mathlib.Meta.FunProp.LambdaTheorem
-- Mathlib.Tactic.Abel
/-- The `AddCommGroup α` or `AddCommMonoid α` expression.  -/
Mathlib.Tactic.Abel.Context.inst : Mathlib.Tactic.Abel.Context → Lean.Expr
-- Mathlib.Algebra.Order.Floor.Ring
Int.div_two_lt_floor : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a : k},
  1 ≤ a → a / 2 < ↑⌊a⌋
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_eq_of_subset : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] {p : Polynomial R} (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → ∀ {s : Finset ℕ}, p.support ⊆ s → p.sum f = ∑ n ∈ s, f n (p.coeff n)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_tensorProduct' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N),
  (LinearMap.trace R (TensorProduct R M N)) (TensorProduct.map f g) = (LinearMap.trace R M) f * (LinearMap.trace R N) g
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_negSucc : ∀ (m n : ℕ), Int.negSucc m <<< ↑n = Int.negSucc (Nat.shiftLeft' true m n)
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.initCache : Lean.ForEachExprWhere.State
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The canonical factor `CanonicalFactor R w` has a simple pole at `z = w`.
 -/
Complex.meromorphicOrderAt_canonicalFactor : ∀ {R : ℝ} {w : ℂ}, w ∈ Metric.ball 0 R → meromorphicOrderAt (Complex.canonicalFactor R w) w = -1
-- Mathlib.Topology.Path
/-- The following instance defines the topology on the path space to be induced from the
compact-open topology on the space `C(I,X)` of continuous maps from `I` to `X`.
 -/
Path.instTopologicalSpace : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → TopologicalSpace (Path x y)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.mk.inj : ∀ {T : Type u_1} {NT : Type} {initial : NT} {rules : Finset (ContextFreeRule T NT)} {NT_1 : Type} {initial_1 : NT_1}
  {rules_1 : Finset (ContextFreeRule T NT_1)},
  { NT := NT, initial := initial, rules := rules } = { NT := NT_1, initial := initial_1, rules := rules_1 } →
    NT = NT_1 ∧ initial ≍ initial_1 ∧ rules ≍ rules_1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafAddCommGroup.compLeft.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [inst_7 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E H')
  (M : Type u) [inst_8 : TopologicalSpace M] [inst_9 : ChartedSpace HM M] (A A' : Type u) [inst_10 : TopologicalSpace A]
  [inst_11 : ChartedSpace H A] [inst_12 : TopologicalSpace A'] [inst_13 : ChartedSpace H' A'] [inst_14 : AddCommGroup A]
  [inst_15 : AddCommGroup A'] [inst_16 : LieAddGroup I (↑⊤) A] [inst_17 : LieAddGroup I' (↑⊤) A'] (φ : A →+ A')
  (hφ : ContMDiff I I' ↑⊤ ⇑φ),
  smoothSheafAddCommGroup.compLeft IM I I' M A A' φ hφ =
    CategoryTheory.ObjectProperty.homMk
      { app := fun x => AddCommGrpCat.ofHom (ContMDiffMap.compLeftAddMonoidHom IM (↥(Opposite.unop x)) φ hφ),
        naturality := ⋯ }
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear maps
on the underlying module. In the case that these two maps are identical, this is the usual concept
of self adjointness. In the case that one of the maps is the negation of the other, this is the
usual concept of skew adjointness.  -/
LinearMap.IsPairSelfAdjoint : {R : Type u_1} →
  {M : Type u_5} →
    {M₁ : Type u_6} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid M₁] →
              [inst_4 : Module R M₁] → {I : R →+* R} → (M →ₗ[R] M →ₛₗ[I] M₁) → (M →ₗ[R] M →ₛₗ[I] M₁) → (M → M) → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.zero_eq_bot : ∀ {X : AlgebraicGeometry.Scheme}, 0 = ⊥
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.self_Ring : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (Algebra.Extension.self R S).Ring = S
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_ofSubring : ∀ {K : Type u} [inst : Field K] (R : Subring K) (hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) (x : K),
  x ∈ ValuationSubring.ofSubring R hR ↔ x ∈ R
-- Init.System.IO
/-- Arguments for the command.  -/
IO.Process.SpawnArgs.args : IO.Process.SpawnArgs → Array String
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedGroupInfo : Inhabited Std.Internal.UV.System.GroupInfo
-- Mathlib.Order.ModularLattice
infIccOrderIsoIccSup_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (x : ↑(Set.Icc (a ⊓ b) a)),
  ↑((infIccOrderIsoIccSup a b) x) = ↑x ⊔ b
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel κ.swapRight
-- Mathlib.Data.Finsupp.Single
Finsupp.update_comm : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) {a₁ a₂ : α},
  a₁ ≠ a₂ → ∀ (m₁ m₂ : M), (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Units.val_cfcRpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : Aˣ) (x : ℝ) (ha : autoParam (0 ≤ ↑a) Units.cfcRpow._auto_1),
  ↑(a.cfcRpow x ha) = ↑a ^ x
-- Mathlib.Data.Set.Subset
Set.preimage_val_eq_univ_of_subset : ∀ {α : Type u_2} {A B : Set α}, A ⊆ B → Subtype.val ⁻¹' B = Set.univ
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instIsEquivalenceFGModuleCatEmbed : ∀ (R : Type u) [inst : Ring R], (FGModuleRepr.embed R).IsEquivalence
-- Lean.Meta.Eval
Lean.Meta.evalExprCore : (α : Type) →
  Lean.Expr →
    (Lean.Expr → Lean.MetaM Unit) →
      optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe → optParam Bool true → Lean.MetaM α
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivProdDFinsupp_add : ∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → AddZeroClass (α i)] (f g : Π₀ (i : Option ι), α i),
  DFinsupp.equivProdDFinsupp (f + g) = DFinsupp.equivProdDFinsupp f + DFinsupp.equivProdDFinsupp g
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusion_homMk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b)
  [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ],
  CategoryTheory.Functor.Fiber.fiberInclusion.map (CategoryTheory.Functor.Fiber.homMk p S φ) = φ
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.total_le : ∀ {α : Type u_1} [inst : LinearOrder α], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.FieldTheory.KummerPolynomial
root_X_pow_sub_C_ne_zero : ∀ {K : Type u} [inst : Field K] {n : ℕ}, 1 < n → ∀ (a : K), AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples : ∀ (T : ℝ) [hT : Fact (0 < T)],
  MeasureTheory.HasAddFundamentalDomain ↥(AddSubgroup.zmultiples T).op ℝ MeasureTheory.volume
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.ext_to_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  ¬c.Rel i (c.next i) →
    ∀ {A : C} {f g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i},
      CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.sndX φ i) =
          CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.sndX φ i) →
        f = g
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.map : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {p : Polynomial R},
  p.Separable → ∀ {f : R →+* S}, (Polynomial.map f p).Separable
-- Init.Data.BitVec.Basic
/-- We prefer `x[i]` as the simp normal form for `getLsb'`  -/
BitVec.getLsb_eq_getElem : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getLsb i = x[i]
-- Mathlib.Algebra.Field.IsField
IsField.mk : ∀ {R : Type u} [inst : Semiring R],
  (∃ x y, x ≠ y) → (∀ (x y : R), x * y = y * x) → (∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1) → IsField R
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_subset_nsmul_add_of_sq_subset_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α} {n : ℕ},
  2 • s ⊆ t + s → n ≠ 0 → n • s ⊆ (n - 1) • t + s
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_sSup_le : ∀ {c : Cardinal.{u}} {s : Set Ordinal.{u}},
  Cardinal.mk ↑s ≤ Cardinal.lift.{u + 1, u} c → (∀ x ∈ s, x.card ≤ c) → (sSup s).card ≤ c
-- Mathlib.Analysis.SpecialFunctions.Sqrt
/-- Local homeomorph between `(0, +∞)` and `(0, +∞)` with `toFun = (· ^ 2)` and
`invFun = Real.sqrt`.  -/
Real.sqPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The measurable equivalence for (dependent) functions on an Option type
`(∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none`.  -/
MeasurableEquiv.piOptionEquivProd : {δ : Type u_8} →
  (α : Option δ → Type u_9) →
    [inst : (i : Option δ) → MeasurableSpace (α i)] → ((i : Option δ) → α i) ≃ᵐ ((i : δ) → α (some i)) × α none
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curry_uncurry : ∀ {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : Function.FromTypes p τ), Function.FromTypes.curry f.uncurry = f
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- For `g : F.obj X → F.obj X`, this is the element in the fiber of the self product,
which has at index `x : F.obj X` the element `g x`.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.mkSelfProdFib : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X : C) → (F.obj (CategoryTheory.PreGaloisCategory.selfProd✝ F X)).obj
-- Mathlib.Algebra.Tropical.Basic
Tropical.instMulOneClassTropical : {R : Type u} → [AddZeroClass R] → MulOneClass (Tropical R)
-- Mathlib.Algebra.Order.Floor.Ring
Int.mul_lt_floor : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a b : k},
  0 < b → b < 1 → ↑⌈b / (1 - b)⌉ ≤ a → b * a < ↑⌊a⌋
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The space of paths with both endpoints equal to a specified point `x : X`.
Denoted as `Ω`, within the `Topology.Homotopy` namespace.  -/
LoopSpace : (X : Type u_2) → [TopologicalSpace X] → X → Type u_2
-- Init.Data.Nat.Lemmas
Nat.pow_sub_mul_pow : ∀ (a : ℕ) {m n : ℕ}, m ≤ n → a ^ (n - m) * a ^ m = a ^ n
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_neg : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G), -⁅g₁, g₂⁆ = ⁅g₂, g₁⁆
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_le_one_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v.restrict x ≤ 1 ↔ v x ≤ 1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} (t : Lean.Elab.Tactic.TacticParsedSnapshot)
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_1 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_10 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.arithShiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_10 w n lhs rhs
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_unitIso_hom_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.π_comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : J.R)
  {Z : C} (h : K₂.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.π b) (CategoryTheory.CategoryStruct.comp f.hom h) =
    CategoryTheory.CategoryStruct.comp (K₂.π b) h
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.assoc' : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_3} (F : FormalGroup R) {f₀ f₁ f₂ : MvPowerSeries σ R},
  PowerSeries.HasSubst f₀ →
    PowerSeries.HasSubst f₁ →
      PowerSeries.HasSubst f₂ →
        MvPowerSeries.subst ![MvPowerSeries.subst ![f₀, f₁] F.toPowerSeries, f₂] F.toPowerSeries =
          MvPowerSeries.subst ![f₀, MvPowerSeries.subst ![f₁, f₂] F.toPowerSeries] F.toPowerSeries
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_eq_prev?_toSlice : ∀ {s : String} {p : s.Pos}, p.prev? = Option.map String.Pos.ofToSlice p.toSlice.prev?