mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.equivEssImageOfReflective_inverse : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i],
  CategoryTheory.equivEssImageOfReflective.inverse = i.essImage.ι.comp (CategoryTheory.reflector i)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk.sizeOf_spec : ∀ {A : Type u_9} {B : Type u_10} [inst : Add A] [inst_1 : Add B] [inst_2 : SizeOf A] [inst_3 : SizeOf B]
  (toEquiv : A ≃ B) (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y),
  sizeOf { toEquiv := toEquiv, map_add' := map_add' } = 1 + sizeOf toEquiv
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt_eq : ∀ (q : ℚ), Rat.sqrt (q * q) = |q|
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.LeftHomotopyRel f g →
    ∀ {Z : C} (p : Y ⟶ Z),
      HomotopicalAlgebra.LeftHomotopyRel (CategoryTheory.CategoryStruct.comp f p)
        (CategoryTheory.CategoryStruct.comp g p)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₁_totalShift₂XIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁'),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁)
      (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow •
      CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_eq_empty_iff : ∀ {b : ByteArray} {i j : ℕ}, b.extract i j = ByteArray.empty ↔ min j b.size ≤ i
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If `i : Fin (n + 2)`, this is the order isomorphism between `Fin (n +1)`
and the complement of `{i}` as a finset.  -/
SSet.stdSimplex.finSuccAboveOrderIsoFinset : {n : ℕ} → (i : Fin (n + 2)) → Fin (n + 1) ≃o ↥{i}ᶜ
-- Mathlib.Data.Finmap
Finmap.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (entries : Multiset (Sigma β))
  (nodupKeys : entries.NodupKeys),
  sizeOf { entries := entries, nodupKeys := nodupKeys } = 1 + sizeOf entries + sizeOf nodupKeys
-- Lean.ProjFns
Lean.instInhabitedAuxParentProjectionInfo.default : Lean.AuxParentProjectionInfo
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : LawfulBEq α]
  [inst_1 : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = m.get! a
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀ : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : Monoid M]
  [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → M},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ProbabilityTheory.IndepFun f g μ →
        MeasureTheory.Measure.map (f * g) μ = (MeasureTheory.Measure.map f μ).mconv (MeasureTheory.Measure.map g μ)
-- Mathlib.MeasureTheory.Order.Lattice
/-- Eta-expanded form of `AEMeasurable.inf` -/
AEMeasurable.fun_inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Min M] [MeasurableInf₂ M],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i ⊓ g i) μ
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.mono : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, t.IsPWO → s ⊆ t → s.IsPWO
-- Mathlib.RingTheory.Valuation.PrimeMultiplicity
multiplicity_addValuation_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : R} {hp : Prime p} {r : R},
  (multiplicity_addValuation hp) r = emultiplicity p r
-- Mathlib.Analysis.ODE.ExistUnique
/-- If a vector field `f : E → E` is continuously differentiable at `x₀ : E`, then it admits an
integral curve `α : ℝ → E` defined on an open interval, with initial condition `α t₀ = x`, where
`x` may be different from `x₀`.  -/
ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∀ (t₀ : ℝ),
      ∃ r > 0,
        ∃ ε > 0, ∀ x ∈ Metric.closedBall x₀ r, ∃ α, α t₀ = x ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite' : ∀ {b : Bool} {a : BitVec 1}, (b == (a == 1#1)) = (a == bif b then 1#1 else 0#1)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.instFaithfulFibι : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [inst_2 : HasFibers p] (S : 𝒮), (HasFibers.ι S).Faithful
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.mem_toTwoSided : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] {x : R}, x ∈ I.toTwoSided ↔ x ∈ I
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_iff_forall_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G],
  AddGroup.ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : AddSubgroup G) [H.FiniteIndex], g ∈ H) → g = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_2 : ∀ (k : Turing.PartrecToTM2.K') (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ')
  (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.push k f q) =
    Turing.TM2.Stmt.branch (fun s => (f s).isSome)
      (Turing.TM2.Stmt.push k (fun s => (f s).getD default) (Turing.TM2.Stmt.goto fun x => q))
      (Turing.TM2.Stmt.goto fun x => q)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (X_1 : ↑(Set.Iic j)),
  (CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso hj F τ).hom.app X_1 =
    (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ ↑X_1 ⋯).hom
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.seq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (q : PMF (α → β)) (p : PMF α), q.seq p = q.bind fun m => p.bind fun a => PMF.pure (m a)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A complete `r`-partite graph has no `n`-cliques for `r < n`.  -/
SimpleGraph.cliqueFree_completeMultipartiteGraph : ∀ {n : ℕ} {ι : Type u_3} [inst : Fintype ι] (V : ι → Type u_4),
  Fintype.card ι < n → (SimpleGraph.completeMultipartiteGraph V).CliqueFree n
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.pow_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Monoid γ] [inst_3 : ContinuousMul γ] (f : α →ₘ[μ] γ) (n : ℕ), (f ^ n).toGerm = f.toGerm ^ n
-- Mathlib.Order.Irreducible
SupIrred.ne_bot : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α} [inst_1 : OrderBot α], SupIrred a → a ≠ ⊥
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₃_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃},
  c₃.Rel i₃ i₃' → ∀ (j : ι₄), ⋯ = ⋯
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : Nontrivial R] (v : AbsoluteValue R ℝ) (x : R),
  (MulRingNorm.mulRingNormEquivAbsoluteValue.symm v) x = v x
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.prodComparison_algSpec_left : ∀ {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ),
  CategoryTheory.Over.Hom.left
      (CategoryTheory.CartesianMonoidalCategory.prodComparison (AlgebraicGeometry.algSpec R) X Y) =
    (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).inv
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.irreducible_iff_prime_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M],
  (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
-- Mathlib.Order.DirSupClosed
/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets in `D`.
This is the complement of a `DirSupClosedOn` set.  -/
DirSupInaccOn : {α : Type u_1} → [Preorder α] → Set (Set α) → Set α → Prop
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_zero : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, OrdinalApprox.lfpApprox f x 0 = x
-- Mathlib.Analysis.Calculus.DifferentialForm.VectorField
/-- Let `ω` be a differentiable `n`-form and `V i` be `n + 1` differentiable vector fields.
If `V i` pairwise commute at `x`, i.e., $[V_i, V_j](x) = 0$ for all `i ≠ j`, then

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) = \sum_{i=0}^{n + 1} (-1)^i •
    D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)).
$$
 -/
extDeriv_apply_vectorField_of_pairwise_commute : ∀ {𝕜 : 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] {n : ℕ} {x : E}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {V : Fin (n + 1) → E → E},
  DifferentiableAt 𝕜 ω x →
    (∀ (i : Fin (n + 1)), DifferentiableAt 𝕜 (V i) x) →
      (Pairwise fun i j => VectorField.lieBracket 𝕜 (V i) (V j) x = 0) →
        ((extDeriv ω x) fun x_1 => V x_1 x) =
          ∑ i, (-1) ^ ↑i • (fderiv 𝕜 (fun x => (ω x) (i.removeNth fun x_1 => V x_1 x)) x) (V i x)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A finitely supported probability distribution over elements of `M` with coefficients in `R`.
The weights are non-negative and sum to 1.
 -/
Convexity.StdSimplex : (R : Type u) → [LE R] → [AddCommMonoid R] → [One R] → Type v → Type (max u v)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_iff_getKey?_eq_some_and_getValue?_eq_some : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    (⟨k, v⟩ ∈ l ↔ Std.Internal.List.getKey? k l = some k ∧ Std.Internal.List.getValue? k l = some v)
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.congr_arg : ∀ {α : Sort u} {f : Equiv.Perm α} {x x' : α}, x = x' → f x = f x'
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.isEmpty_iff_toList_eq_nil : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp}, t.isEmpty = true ↔ t.toList = []
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.prod.eq_def : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (x : ℕ) (x_1 : Fin x → α),
  FinVec.prod x_1 =
    match x, x_1 with
    | 0, x => 1
    | 1, v => v 0
    | n.succ.succ, v => (FinVec.prod fun i => v i.castSucc) * v (Fin.last (n + 1))
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_concat : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (x.concat b).cpop.toNat = b.toNat + x.cpop.toNat
-- Aesop.Tree.Data
Aesop.instInhabitedNormalizationState.default : Aesop.NormalizationState
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸}, DifferentiableOn 𝕜 a s → ∀ (b : 𝔸), DifferentiableOn 𝕜 (fun y => a y * b) s
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- Reverse the direction of a path.  -/
Quiver.Path.reverse : {V : Type u_2} → [inst : Quiver V] → [Quiver.HasReverse V] → {a b : V} → Quiver.Path a b → Quiver.Path b a
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.addRight.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  Homeomorph.addRight a = { toEquiv := Equiv.addRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Elab.Do.Basic
/-- Set the new `do` block result type for the scope of the continuation `k`.  -/
Lean.Elab.Do.withDoBlockResultType : {α : Type} → Lean.Expr → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Lean.Data.FuzzyMatching
/-- Represents a fuzzy matching score where `Score.awful` is the worst score possible.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score : Type
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.lift_of_apply : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (x : X), ((FreeLieAlgebra.lift R) f) (FreeLieAlgebra.of R x) = f x
-- Mathlib.CategoryTheory.EpiMono
/-- A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X`
such that `f ≫ retraction f = 𝟙 X`.

Every split monomorphism is a monomorphism.
 -/
CategoryTheory.SplitMono : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Type v₁
-- Init.Data.Option.Lemmas
Option.isSome.eq_1 : ∀ {α : Type u_1} (val : α), (some val).isSome = true
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point.  -/
MDifferentiableWithinAt.prodMap' : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {f : M → M'} {g : N → N'} {r : Set N} {p : M × N},
  MDiffAt[s] f p.1 → MDiffAt[r] g p.2 → MDiffAt[s ×ˢ r] (Prod.map f g) p
-- Mathlib.Tactic.Algebra.Basic
/-- Take an expression `r'` in a ring `R'` such that `R` is an `R'`-algebra and cast `r'` to `R`
using `algebraMap R' R`, so that the scalar multiplication action on `A` is preserved.  -/
Mathlib.Tactic.Algebra.RingCompute.cast : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Algebra.Cache sR →
              (u' : Lean.Level) →
                (R' : Q(Type u')) →
                  Q(CommSemiring «$R'») →
                    (_smul : Q(SMul «$R'» «$A»)) →
                      (r' : Q(«$R'»)) →
                        Mathlib.Tactic.AtomM
                          ((y : Q(«$A»)) ×
                            Mathlib.Tactic.Ring.Common.ExSum (Mathlib.Tactic.Algebra.BaseType sAlg) sA q(«$y») ×
                              Q(∀ (a : «$A»), «$r'» • a = «$y» * a))
-- Mathlib.CategoryTheory.Localization.Construction
/-- A `MorphismProperty` in `W.Localization` is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, if is stable under composition
and if the property is stable by passing to inverses.  -/
CategoryTheory.Localization.Construction.morphismProperty_eq_top' : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
  (P : CategoryTheory.MorphismProperty W.Localization) [P.IsStableUnderComposition],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) → (∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y), P e.hom → P e.inv) → P = ⊤
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instFromJsonPosition : Lean.FromJson Lean.Lsp.Position
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.mk.inj : ∀ {J : Type u_1} {inst : LinearOrder J} {i j : J} {I : Set J}
  {left : autoParam (i ∈ I) CategoryTheory.SimplicialThickening.Path.left._autoParam}
  {right : autoParam (j ∈ I) CategoryTheory.SimplicialThickening.Path.right._autoParam}
  {left_le : autoParam (∀ k ∈ I, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam}
  {le_right : autoParam (∀ k ∈ I, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam} {I_1 : Set J}
  {left_1 : autoParam (i ∈ I_1) CategoryTheory.SimplicialThickening.Path.left._autoParam}
  {right_1 : autoParam (j ∈ I_1) CategoryTheory.SimplicialThickening.Path.right._autoParam}
  {left_le_1 : autoParam (∀ k ∈ I_1, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam}
  {le_right_1 : autoParam (∀ k ∈ I_1, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam},
  { I := I, left := left, right := right, left_le := left_le, le_right := le_right } =
      { I := I_1, left := left_1, right := right_1, left_le := left_le_1, le_right := le_right_1 } →
    I = I_1
-- Init.Data.String.OrderInstances
String.Pos.Raw.instLTCiOfNatInt : Lean.Grind.ToInt.LT String.Pos.Raw (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instTop.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  AddSubgroup.instTop =
    {
      top :=
        let __src := ⊤;
        { toAddSubmonoid := __src, neg_mem' := ⋯ } }
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Copy of an intermediate field with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
IntermediateField.copy : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (S : IntermediateField K L) → (s : Set L) → s = ↑S → IntermediateField K L
-- Mathlib.Order.Sublattice
/-- The preimage of a sublattice along a lattice homomorphism.  -/
Sublattice.comap : {α : Type u_2} →
  {β : Type u_3} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → Sublattice β → Sublattice α
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.smul_single : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (c : R) (a : α) (b : M),
  (c • fun₀ | a => b) = fun₀ | a => c • b
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.isoToPlus.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  (hP : CategoryTheory.Presheaf.IsSheaf J P), J.isoToPlus P hP = J.isoToPlus P hP
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.bisim' : ∀ {P : PFunctor.{uA, uB}} {α : Type u_3} (Q : α → Prop) (u v : α → P.M),
  (∀ (x : α),
      Q x →
        ∃ a f f', (u x).dest = ⟨a, f⟩ ∧ (v x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') →
    ∀ (x : α), Q x → u x = v x
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_t_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] {X Y : C} (f : X ⟶ Y)
  (hf : W f) (g : X ⟶ Z) {Z_1 : C} (h : ∐ CategoryTheory.OrthogonalReflection.D₁.obj₂ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.t W Z) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιRight f hf g) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_congr : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a b : α},
      compare a b = Ordering.eq → Std.DTreeMap.Internal.Impl.Const.get? t a = Std.DTreeMap.Internal.Impl.Const.get? t b
-- Mathlib.Data.List.Destutter
/-- `List.destutter` on a relation like ≠, whose negation is an equivalence, has length
monotone under List.cons  -/
List.length_destutter_le_length_destutter_cons : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a : α} [IsEquiv α Rᶜ] {l : List α},
  (List.destutter R l).length ≤ (List.destutter R (a :: l)).length
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_smul_adjp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A B : Matrix n n R},
  A * B = 1 →
    A + (Matrix.detp 1 A • Matrix.adjp (-1) B + Matrix.detp (-1) A • Matrix.adjp 1 B) =
      Matrix.detp 1 A • Matrix.adjp 1 B + Matrix.detp (-1) A • Matrix.adjp (-1) B
-- Mathlib.Algebra.Star.Subsemiring
/-- The center of a semiring `R` is the set of elements that commute and associate with everything
in `R`  -/
StarSubsemiring.center : (R : Type u_1) → [inst : NonAssocSemiring R] → [inst_1 : StarRing R] → StarSubsemiring R
-- Mathlib.Order.BoundedOrder.Basic
Subtype.coe_bot : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : OrderBot (Subtype p)],
  p ⊥ → ↑⊥ = ⊥
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.foldrM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} → [Monad m] → ((a : α) → β a → δ → m δ) → δ → Std.DHashMap.Internal.AssocList α β → m δ