mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.tr.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2to1.Λ' K Γ Λ σ → Sort u_5) (k : K)
  (s : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) (h_1 : (q : Λ) → motive (Turing.TM2to1.Λ'.normal q))
  (h_2 : (k : K) → (s : Turing.TM2to1.StAct K Γ σ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.go k s q))
  (h_3 : (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2to1.Λ'.ret q)),
  (match Turing.TM2to1.Λ'.go k s q with
    | Turing.TM2to1.Λ'.normal q => h_1 q
    | Turing.TM2to1.Λ'.go k s q => h_2 k s q
    | Turing.TM2to1.Λ'.ret q => h_3 q) =
    h_2 k s q
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.motives.pi : Lean.Option Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGED_eq_getD_getEntryGE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} {fallback : (a : α) × β a},
  Std.DTreeMap.Internal.Impl.getEntryGED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGE? k t).getD fallback
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitBy_append_of_isChain : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (hn : l ≠ []),
  List.IsChain (fun x y => r x y = true) l →
    (∀ x ∈ m.head?, r (l.getLast hn) x = false) → List.splitBy r (l ++ m) = l :: List.splitBy r m
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.isChain_cons_of_isChain_cons_cons`. -/
List.chain_of_chain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → List.IsChain R (b :: l)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_neg_one : Real.arcsin (-1) = -(Real.pi / 2)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Cache.mk.sizeOf_spec : ∀ (backwardRuleName : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule)
  (backwardRuleSyntax : Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule)
  (simpState : Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State)
  (dsimpState : Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State),
  sizeOf
      { backwardRuleName := backwardRuleName, backwardRuleSyntax := backwardRuleSyntax, simpState := simpState,
        dsimpState := dsimpState } =
    1 + sizeOf backwardRuleName + sizeOf backwardRuleSyntax + sizeOf simpState + sizeOf dsimpState
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalTorsor : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G], IsTopologicalTorsor G
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get!.eq_2 : ∀ {α : Type u} {δ : Type w} [inst : Ord α] [inst_1 : Inhabited δ] (k : α) (size : ℕ) (k' : α) (v' : δ)
  (l r : Std.DTreeMap.Internal.Impl α fun x => δ),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.inner size k' v' l r) k =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get! l k
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get! r k
    | Ordering.eq => v'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} {l : List α} {k : α},
  t.insertManyIfNewUnit (k :: l) = (t.insertIfNew k ()).insertManyIfNewUnit l
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_ratCast_atTop_iff : ∀ {α : Type u_1} {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R]
  {f : α → ℚ} {l : Filter α}, Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_countableGeneratingSet : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α],
  MeasurableSpace.generateFrom (MeasurableSpace.countableGeneratingSet α) = m
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RcoSliceData α β → Std.Rco α
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.coe_rpow_of_nonneg : ∀ (x : NNReal) {y : ℝ}, 0 ≤ y → ↑(x ^ y) = ↑x ^ y
-- Init.Data.UInt.Lemmas
UInt64.toFin_add : ∀ (a b : UInt64), (a + b).toFin = a.toFin + b.toFin
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_eq_get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {h : a ∈ t}, t.get a h = (t.get? a).get ⋯
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.ext : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst_1 : Monoid G} {M N : Action V G}
  {x y : M.Hom N}, x.hom = y.hom → x = y
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.IterM.toListRev_toIter : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.IterM Id β},
  it.toIter.toListRev = it.toListRev.run
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The n-coskeleton as an endofunctor on `SimplicialObject C`.  -/
CategoryTheory.SimplicialObject.cosk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
        CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject C)
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupMap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H : Subgroup G),
  f.subgroupMap H = f.submonoidMap H.toSubmonoid
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap.match_1.eq_2 : ∀ {C₀ : Type u_4} {C : Type u_5} [inst : CategoryTheory.Category.{u_2, u_4} C₀]
  [inst_1 : CategoryTheory.Category.{u_3, u_5} C] {F : CategoryTheory.Functor C₀ C} {X : C}
  (data : F.PreOneHypercoverDenseData X)
  (motive : CategoryTheory.Limits.WalkingMulticospan data.multicospanShape → Sort u_6) (j : data.multicospanShape.R)
  (h_1 : (i : data.multicospanShape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (j : data.multicospanShape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right j)),
  (match CategoryTheory.Limits.WalkingMulticospan.right j with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right j => h_2 j) =
    h_2 j
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp) (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ t),
  Std.ExtDTreeMap.Const.get t a h = Std.ExtDTreeMap.Const.get t_1 a_1 ⋯
-- Lean.Util.Diff
Lean.Diff.Histogram.Entry.mk.injEq : ∀ {α : Type u} {lsize rsize : ℕ} (leftCount : ℕ) (leftIndex : Option (Fin lsize))
  (leftWF : leftCount = 0 ↔ leftIndex = none) (rightCount : ℕ) (rightIndex : Option (Fin rsize))
  (rightWF : rightCount = 0 ↔ rightIndex = none) (leftCount_1 : ℕ) (leftIndex_1 : Option (Fin lsize))
  (leftWF_1 : leftCount_1 = 0 ↔ leftIndex_1 = none) (rightCount_1 : ℕ) (rightIndex_1 : Option (Fin rsize))
  (rightWF_1 : rightCount_1 = 0 ↔ rightIndex_1 = none),
  ({ leftCount := leftCount, leftIndex := leftIndex, leftWF := leftWF, rightCount := rightCount,
        rightIndex := rightIndex, rightWF := rightWF } =
      { leftCount := leftCount_1, leftIndex := leftIndex_1, leftWF := leftWF_1, rightCount := rightCount_1,
        rightIndex := rightIndex_1, rightWF := rightWF_1 }) =
    (leftCount = leftCount_1 ∧ leftIndex = leftIndex_1 ∧ rightCount = rightCount_1 ∧ rightIndex = rightIndex_1)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
/-- The image of a tangent cone under the differential of a map is included in the tangent cone to
the image.  -/
HasFDerivWithinAt.mapsTo_tangent_cone : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {f' : E →L[𝕜] F} {x : E},
  HasFDerivWithinAt f f' s x → Set.MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a b : α}, (a == b) = true → m[a]! = m[b]!
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (k : K) (f : σ → Γ k)
  (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.push k f q, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_1 k f q v S
-- Mathlib.Data.List.Sort
/-- Another statement of stability of insertion sort.
If a pair `[a, b]` is a sublist of `l` and `r a b`,
then `[a, b]` is still a sublist of `insertionSort r l`.
 -/
List.pair_sublist_insertionSort : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] {a b : α} {l : List α},
  r a b → [a, b].Sublist l → [a, b].Sublist (List.insertionSort r l)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.symm_trans_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : Star A] [inst_5 : Star B] [inst_6 : Add C] [inst_7 : Mul C] [inst_8 : Star C] (e₁ : A ≃⋆+* B)
  (e₂ : B ≃⋆+* C) (x : C), (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
-- Mathlib.Order.Ideal
Order.Ideal.lt_sup_principal_of_notMem : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : IsCodirectedOrder P] {x : P} {I : Order.Ideal P},
  x ∉ I → I < I ⊔ Order.Ideal.principal x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalCommRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalCommRing β] → [IsTopologicalRing β] → NonUnitalCommRing (ZeroAtInftyContinuousMap α β)
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the pair `(t.contains k, t.insertIfNew k v)`.  -/
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (k : α) →
        β k →
          (t : Std.DTreeMap.Internal.Impl α β) →
            t.Balanced → Bool × Std.DTreeMap.Internal.Impl.SizedBalancedTree α β t.size (t.size + 1)
-- Mathlib.Data.Finsupp.SMul
/-- Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range.
See the `instance_diamonds` test for examples of such conflicts.  -/
Finsupp.comapSMul : {α : Type u_1} →
  {M : Type u_3} → {G : Type u_5} → [inst : Monoid G] → [MulAction G α] → [inst : AddCommMonoid M] → SMul G (α →₀ M)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.const_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Sub γ] [MeasurableSub γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => c - f x) (fun x => c - g x) μ ν
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If the measure `μ` is separable (in particular if `X` is countably generated and `μ` is
`s`-finite), if `E` is a second-countable `NormedAddCommGroup`, and if `1 ≤ p < +∞`,
then the associated `Lᵖ` space is second-countable.  -/
MeasureTheory.Lp.SecondCountableTopology : ∀ {X : Type u_1} {E : Type u_2} [m : MeasurableSpace X] [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  {p : ENNReal} [one_le_p : Fact (1 ≤ p)] [p_ne_top : Fact (p ≠ ⊤)] [MeasureTheory.IsSeparable μ]
  [TopologicalSpace.SeparableSpace E], SecondCountableTopology ↥(MeasureTheory.Lp E p μ)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.lift_cardinalMk_adjoin_le : ∀ (F : Type u) [inst : Field F] {E : Type v} [inst_1 : Field E] [inst_2 : Algebra F E] (s : Set E),
  Cardinal.lift.{u, v} (Cardinal.mk ↥(IntermediateField.adjoin F s)) ≤
    max (max (Cardinal.lift.{v, u} (Cardinal.mk F)) (Cardinal.lift.{u, v} (Cardinal.mk ↑s))) Cardinal.aleph0
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioc_pred_left_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] [NoMinOrder α] (a b : α),
  Finset.Ioc (Order.pred a) b = Finset.Icc a b
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.hasStrictDerivAt_log : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt Real.log x⁻¹ x
-- Lean.Parser.Term.Basic
/-- Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
 -/
Lean.Parser.Term.explicitBinder : optParam Bool false → Lean.Parser.Parser
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.zero_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (β : Type w) (X Y : CategoryTheory.GradedObject β C) (b : β), 0 b = 0
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_eq : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  (∀ s < r, f s ≤ x) → (∀ s > r, x ≤ f s) → ArchimedeanClass.stdPart x = r
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.ext_iff : ∀ {α : Type u_1} {p q : PMF α}, p = q ↔ ∀ (x : α), p x = q x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_iff_toList_perm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.mk.inj : ∀ {α : Type u} {β : α → Type v} {size : ℕ} {buckets : Array (Std.DHashMap.Internal.AssocList α β)} {size_1 : ℕ}
  {buckets_1 : Array (Std.DHashMap.Internal.AssocList α β)},
  { size := size, buckets := buckets } = { size := size_1, buckets := buckets_1 } → size = size_1 ∧ buckets = buckets_1
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_iSup_apply : ∀ {E : Type u_3} [inst : AddGroup E] {ι : Type u_6} (f : ι → AddGroupSeminorm E),
  BddAbove (Set.range f) → ∀ {x : E}, (⨆ i, f i) x = ⨆ i, (f i) x
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppLValsAux : Array Lean.Elab.Term.NamedArg →
  Array Lean.Elab.Term.Arg →
    Option Lean.Expr → Bool → Bool → Lean.Expr → List Lean.Elab.Term.LVal → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Convex.Side
AffineEquiv.wSameSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P'),
  (AffineSubspace.map (↑f) s).WSameSide (f x) (f y) ↔ s.WSameSide x y
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotate_map_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₃ = f.hom₂
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] ∅ → s ∩ t =ᵐ[μ] ∅
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.match_1.splitter : (motive : Bool → Sort u_1) → (__do_lift : Bool) → (Unit → motive true) → (Unit → motive false) → motive __do_lift
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mul_self_mem : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) (x : R), x * x ∈ P
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- The range of a finite additive group under an additive group homomorphism is finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
presence of `Fintype N`.  -/
AddMonoidHom.fintypeRange : {G : Type u_1} →
  [inst : AddGroup G] →
    {N : Type u_3} → [inst_1 : AddGroup N] → [Fintype G] → [DecidableEq N] → (f : G →+ N) → Fintype ↥f.range
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- Given `f : A ⟶ B` a morphism in the category `CommRingCat`, `M : ModuleCat B`,
and `D : M.Derivation f`, this is the induced
morphism `CommRingCat.KaehlerDifferential f ⟶ M`.  -/
ModuleCat.Derivation.desc : {A B : CommRingCat} → {f : A ⟶ B} → {M : ModuleCat ↑B} → M.Derivation f → (CommRingCat.KaehlerDifferential f ⟶ M)
-- Init.Prelude
/-- Boolean equality of natural numbers, usually accessed via the `==` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
Nat.beq : ℕ → ℕ → Bool
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Given two model_with_corners `I` on `(E, H)` and `I'` on `(E', H')`, we define the model with
corners `I.prod I'` on `(E × E', ModelProd H H')`. This appears in particular for the manifold
structure on the tangent bundle to a manifold modelled on `(E, H)`: it will be modelled on
`(E × E, H × E)`. See note [Manifold type tags] for explanation about `ModelProd H H'`
vs `H × H'`.  -/
ModelWithCorners.prod : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type w} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {E' : Type v'} →
                  [inst_4 : NormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      {H' : Type w'} →
                        [inst_6 : TopologicalSpace H'] →
                          ModelWithCorners 𝕜 E' H' → ModelWithCorners 𝕜 (E × E') (ModelProd H H')
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_append_of_not_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l' = false →
    Std.Internal.List.containsKey a (l ++ l') = Std.Internal.List.containsKey a l
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.continuous_φ : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] (x : F), Continuous (NormedAlgebra.Real.φ✝ x)
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_add : ∀ {m n : ℕ}, Even (m + n) ↔ (Even m ↔ Even n)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraDualNumber.equiv_symm_eps : ∀ {R : Type u_1} [inst : CommRing R], CliffordAlgebraDualNumber.equiv.symm DualNumber.eps = (CliffordAlgebra.ι 0) 1
-- Init.Data.Nat.Div.Basic
Nat.mul_div_cancel : ∀ (m : ℕ) {n : ℕ}, 0 < n → m * n / n = m
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoObjConePointsOfIsLimit` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ : CategoryTheory.Limits.IsLimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsLimit c₃) (j : J₁ × J₂) {Z : C} (h : (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).inv
      (CategoryTheory.CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt)
        (CategoryTheory.CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2)) h)) =
    CategoryTheory.CategoryStruct.comp (c₃.π.app j) h
-- Mathlib.Topology.Path
Path.truncate_zero_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), γ.truncate 0 0 = (Path.refl a).cast ⋯ ⋯
-- Mathlib.Algebra.GradedMonoid
/-- Successor powers behave as expected  -/
GradedMonoid.GMonoid.gnpow_succ' : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (n : ℕ) (a : GradedMonoid A),
  GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) =
    ⟨n • a.fst, GradedMonoid.GMonoid.gnpow n a.snd⟩ * a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst.inj : ∀ {x : Int.Internal.Linear.Var} {c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {x_1 : Int.Internal.Linear.Var}
  {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalCommSemiring : {R : Type u_1} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring Rᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage : AlgebraicGeometry.Scheme.etalePrecoverage ≤ AlgebraicGeometry.Scheme.proetalePrecoverage
-- Mathlib.Data.EReal.Inv
EReal.bot_lt_inv : ∀ (x : EReal), ⊥ < x⁻¹
-- Init.Data.Nat.Div.Basic
Nat.div_eq_of_lt : ∀ {a b : ℕ}, a < b → a / b = 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l).getKey! k = default