mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.FaithfullyFlat → Function.Injective ⇑f
-- Mathlib.Data.Finset.Sups
Finset.disjSups_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {a b : α}, {a}.disjSups {b} = if Disjoint a b then {a ⊔ b} else ∅
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ici_of_antitoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) →
    AntitoneOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atBot → f '' Set.Ici a = Set.Iic (f a)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (p : X.Path (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op))
      (SSet.StrictSegalCore.spineToSimplex h p) =
    p.arrow 0
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.eq_1 : ∀ {𝕜 : 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)
  (f' : E →L[𝕜] F) (s : Set E) (c : NNReal),
  ApproximatesLinearOn f f' s c = ∀ x ∈ s, ∀ y ∈ s, ‖f x - f y - f' (x - y)‖ ≤ ↑c * ‖x - y‖
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.instInhabited : (α : Type u_2) → [inst : CompleteLattice α] → Inhabited (CompleteLatticeHom α α)
-- Init.Prelude
/-- Bijection between `α` and `ULift.{v} α`  -/
ULift.up_down : ∀ {α : Type u} (b : ULift.{v, u} α), { down := b.down } = b
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField : (G : Type u_1) →
  [inst : Group G] →
    {K : Type u_2} →
      {L : Type u_3} →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra K L] →
              [inst_4 : MulSemiringAction G L] →
                (F : IntermediateField K L) →
                  (N : Subgroup G) → [inst_5 : N.Normal] → [IsGaloisGroup (↥N) (↥F) L] → MulSemiringAction (G ⧸ N) ↥F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
        P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → W.add P Q = W.dblU P • ![1, 1, 0]
-- Mathlib.Data.Set.Lattice
Set.disjoint_iUnion_left : ∀ {α : Type u_1} {t : Set α} {ι : Sort u_12} {s : ι → Set α}, Disjoint (⋃ i, s i) t ↔ ∀ (i : ι), Disjoint (s i) t
-- Mathlib.Data.Sum.Order
Sum.Lex.lt_def : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α ⊕ₗ β},
  a < b ↔ Sum.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (ofLex a) (ofLex b)
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.isLogEnabledFor : Lean.Options → Lean.Name → Bool
-- Mathlib.Algebra.Order.Positive.Ring
Positive.val_mul : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (x y : { x // 0 < x }),
  ↑(x * y) = ↑x * ↑y
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mul2Shift : USize → USize → USize
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.instReprStatus.repr : Lean.Util.ParamMinimizer.Status → ℕ → Std.Format
-- Mathlib.Data.Sym.Sym2
/-- `fromRel`/`ToRel` induce an order isomorphism between symmetric relations and `Sym2` sets  -/
Sym2.fromRelOrderIso : (α : Type u_1) → { r // Std.Symm r } ≃o Set (Sym2 α)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_id : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α},
  BooleanSubalgebra.map (BoundedLatticeHom.id α) L = L
-- Aesop.Search.Expansion
Aesop.RuleResult.succeeded.sizeOf_spec : ∀ (newRapps : Array Aesop.RappRef), sizeOf (Aesop.RuleResult.succeeded newRapps) = 1 + sizeOf newRapps
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.variance_projectiveFamily : ∀ (I : Finset NNReal) (f : (↥I → ℝ) → ℝ),
  ProbabilityTheory.variance f (ProbabilityTheory.BrownianReal.projectiveFamily I) =
    ProbabilityTheory.variance (f ∘ WithLp.ofLp)
      (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofNat.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive Nat.zero) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | Nat.zero => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.toFun_eq_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X), K.toFun = ⇑K
-- Mathlib.LinearAlgebra.Pi
/-- This is used as the ext lemma instead of `LinearMap.pi_ext` for reasons explained in
note [partially-applied ext lemmas].  -/
LinearMap.pi_ext' : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
  (∀ (i : ι), f ∘ₗ LinearMap.single R φ i = g ∘ₗ LinearMap.single R φ i) → f = g
-- Mathlib.Algebra.Group.End
Equiv.addRight_zero : ∀ {α : Type u_4} [inst : AddGroup α], Equiv.addRight 0 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.R) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.right i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_2 i
-- Std.Http.Data.Method
Std.Http.instDecidableEqMethod : DecidableEq Std.Http.Method
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} {f₁ f₂ : M ⟶ N}, f₁ = f₂ ↔ f₁.hom = f₂.hom
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instSMulIntHom : {M N : AddCommGrpCat} → SMul ℤ (M ⟶ N)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- Bounded closed sets in the weak dual of a separable normed space are sequentially compact.  -/
WeakDual.isSeqCompact_of_isBounded_of_isClosed : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)},
  Bornology.IsBounded s → IsClosed s → IsSeqCompact s
-- Mathlib.Topology.Compactness.NhdsKer
/-- **Alias** of the forward direction of `IsCompact.nhdsKer_iff`. -/
IsCompact.of_nhdsKer : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact (nhdsKer s) → IsCompact s
-- Mathlib.Data.Finset.Slice
Set.sized_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {r : ℕ} {f : (i : ι) → κ i → Set (Finset α)},
  Set.Sized r (⋃ i, ⋃ j, f i j) ↔ ∀ (i : ι) (j : κ i), Set.Sized r (f i j)
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_some : ∀ {α : Type u_1} (s : Multiset α), Multiset.filterMap some s = s
-- Mathlib.Topology.Algebra.FilterBasis
/-- A `GroupFilterBasis` on a group is a `FilterBasis` satisfying some additional axioms.
Example : if `G` is a topological group then the neighbourhoods of the identity are a
`GroupFilterBasis`. Conversely given a `GroupFilterBasis` one can define a topology
compatible with the group structure on `G`.  -/
GroupFilterBasis : (G : Type u) → [Group G] → Type u
-- Mathlib.Topology.Germ
Filter.Germ.sliceRight_coe : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] {x : X} [inst_1 : TopologicalSpace Y] {y : Y}
  (f : X × Y → Z), (↑f).sliceRight = ↑fun y' => f (x, y')
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
/-- An object `X` in an abelian category has projective dimension `≤ n` if
all `Ext X Y i` vanish when `n + 1 ≤ i`  -/
CategoryTheory.HasProjectiveDimensionLE : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → ℕ → Prop
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_coordChange_eq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i j : ι)
  {b : B},
  b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet →
    ∀ (v : F), (Bundle.Trivialization.coordChangeL R (Z.localTriv i) (Z.localTriv j) b) v = (Z.coordChange i j b) v
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isNat_ratDen : ∀ {q : ℚ} {n : ℤ} {n' d : ℕ},
  Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsNat q.den d
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_nilradical : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus ↑(nilradical R) = Set.univ
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.refl : ∀ {α : Type u} {β : Type v} (l : Filter α) (f : α → β), f =ᶠ[l] f
-- Mathlib.Data.Quot
/-- A version of `Quotient.mk` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument.  -/
Quotient.mk'' : {α : Sort u_1} → {s₁ : Setoid α} → α → Quotient s₁
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (E.p₂ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) =
    CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instCoeTC : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → CoeTC R (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.equivOfIsClopen_mk : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ) {i : ι} (x : α) (hx : x ∈ U i),
  (ConnectedComponents.equivOfIsClopen hclopen hdisj hunion) (ConnectedComponents.mk x) =
    ⟨i, ConnectedComponents.mk ⟨x, hx⟩⟩
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ofLeftInverse.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {g : N →* G}
  (h : Function.LeftInverse ⇑g ⇑f),
  MonoidHom.ofLeftInverse h =
    { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Set.Function
Set.surjOn_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Set.SurjOn f ∅ t ↔ t = ∅
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instPartialOrder : {R : Type u_3} → [inst : Add R] → [inst_1 : Mul R] → PartialOrder (RingCon R)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The canonical isomorphism between the chosen biproduct and the chosen product.  -/
CategoryTheory.Limits.biproduct.isoProduct : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) → [inst_2 : CategoryTheory.Limits.HasBiproduct f] → ⨁ f ≅ ∏ᶜ f
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioi_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ioi a)), Subtype.val '' Set.Ici b = Set.Ici ↑b
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosAddRel_of_le : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  (x.1 + x.2).card ≤ (y.1 + y.2).card → y.1.card + y.2.card < x.1.card + x.2.card → DevosAddRel✝ x y
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.congr_simp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f f_1 : 𝕜 → F),
  f = f_1 →
    ∀ (f' f'_1 : F),
      f' = f'_1 →
        ∀ (s s_1 : Set 𝕜),
          s = s_1 → ∀ (x x_1 : 𝕜), x = x_1 → HasDerivWithinAt f f' s x = HasDerivWithinAt f_1 f'_1 s_1 x_1
-- Lean.Parser.Command
Lean.Parser.Command.printTacTags.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_pos_iff_of_nonneg : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M] {f : ι → M}, 0 ≤ f → (0 < ∑ i, f i ↔ 0 < f)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_add : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ ψ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  HomologicalComplex.homologyMap (φ + ψ) i = HomologicalComplex.homologyMap φ i + HomologicalComplex.homologyMap ψ i
-- Init.Data.Int.Gcd
Int.eq_zero_of_gcd_eq_zero_left : ∀ {a b : ℤ}, a.gcd b = 0 → a = 0
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.coeff_μ_tmul : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} {k : Type u} [inst_1 : CommSemiring k]
  (l1 : MonoidAlgebra k X.V) (l2 : MonoidAlgebra k Y.V) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V),
  ((Representation.LinearizeMonoidal.μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2
-- Mathlib.NumberTheory.Real.Irrational
irrational_sub_natCast_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (x - ↑n) ↔ Irrational x
-- Mathlib.Data.Nat.Bits
Nat.div2_succ : ∀ (n : ℕ), (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Connected.toSubgraph : ∀ {V : Type u} {G H : SimpleGraph V} (h : H ≤ G), H.Connected → (SimpleGraph.toSubgraph H h).Connected
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
_private.Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup.0.Matrix.SpecialLinearGroup.diag2_coe.match_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.FBinop
/-- Turn a tree back into an expression.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toExprCore : FBinopElab.Tree✝ → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block  -/
AddAction.IsBlock.of_orbit : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {H : AddSubgroup G} {a : X},
  AddAction.stabilizer G a ≤ H → AddAction.IsBlock G (AddAction.orbit (↥H) a)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_respects_aux₂ : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] {k : K}
  {q : Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ} {v : σ} {S : (k : K) → List (Γ k)}
  {L : Turing.ListBlank ((k : K) → Option (Γ k))},
  (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse) →
    ∀ (o : Turing.TM2to1.StAct K Γ σ k),
      have v' := Turing.TM2to1.stVar v (S k) o;
      have Sk' := Turing.TM2to1.stWrite v (S k) o;
      have S' := Function.update S k Sk';
      ∃ L',
        (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S' k)).reverse) ∧
          Turing.TM1.stepAux (Turing.TM2to1.trStAct q o) v
              ((Turing.Tape.move Turing.Dir.right)^[(S k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L))) =
            Turing.TM1.stepAux q v'
              ((Turing.Tape.move Turing.Dir.right)^[(S' k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L')))
-- Mathlib.Topology.DiscreteSubset
isDiscrete_iff_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s ↔ ∀ x ∈ s, nhdsWithin x s = pure x
-- Mathlib.Data.Rel
/-- The higher-arity graph of a function. Describes α-argument functions from β to β.  -/
Function.tupleGraph : {α : Type u_1} → {β : Type u_2} → ((α → β) → β) → Set (Option α → β)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The functor `P.Comma L R Q W ⥤ P.Comma L R Q W` induced by the identity natural transformation
on `R` is naturally isomorphic to the identity functor.  -/
CategoryTheory.MorphismProperty.Comma.mapRightId : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              CategoryTheory.MorphismProperty.Comma.mapRight L (CategoryTheory.CategoryStruct.id R) ⋯ ≅
                                CategoryTheory.Functor.id (CategoryTheory.MorphismProperty.Comma L R P Q W)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_edgeMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : C} (f : x ⟶ y),
  CategoryTheory.nerve.homEquiv (CategoryTheory.nerve.edgeMk f) = f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.full_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  [G.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.CostructuredArrow.map₂ α β).Full
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGED : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.max!.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : Unit → motive none) (h_2 : (x : α) → motive (some x)),
  (match some x with
    | none => h_1 ()
    | some x => h_2 x) =
    h_2 x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.contains a = false → m.get! a = default
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_vecMulVec : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (u v : n → R),
  (Matrix.vecMulVec u v).charpoly = Polynomial.X ^ Fintype.card n - (u ⬝ᵥ v) • Polynomial.X ^ (Fintype.card n - 1)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- An induction principle for additive closure membership. If `p` holds for `0` and all
elements of `k` and their negation, and is preserved under addition, then `p` holds for all
elements of the additive closure of `k`.  -/
AddSubgroup.closure_induction'' : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (g : G) → g ∈ AddSubgroup.closure s → Prop},
  (∀ (x : G) (hx : x ∈ s), p x ⋯) →
    (∀ (x : G) (hx : x ∈ s), p (-x) ⋯) →
      p 0 ⋯ →
        (∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯) →
          ∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coe_algebraMap : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] {A : Type u_3} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G k A],
  ⇑(algebraMap k (SkewMonoidAlgebra A G)) = SkewMonoidAlgebra.single 1 ∘ ⇑(algebraMap k A)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (m.get x ⋯))
        m.keys.attach).unattach
-- Mathlib.Algebra.DirectSum.Internal
/-- The subring `A 0` of `R`.  -/
SetLike.GradeZero.subring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : Ring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] → [AddSubgroupClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → Subring R
-- Mathlib.Analysis.Convex.Function
/-- Convexity of functions  -/
ConvexOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_5} →
      [Semiring 𝕜] →
        [PartialOrder 𝕜] →
          [AddCommMonoid E] → [AddCommMonoid β] → [PartialOrder β] → [SMul 𝕜 E] → [SMul 𝕜 β] → Set E → (E → β) → Prop
-- Mathlib.LinearAlgebra.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Matrix.SpecialLinearGroup.toLin' =
    { toFun := fun A => LinearEquiv.ofLinearMap (Matrix.toLin' ↑A) (Matrix.toLin' ↑A⁻¹) ⋯ ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.RingTheory.Trace.Basic
trace_eq_finrank_mul_minpoly_nextCoeff : ∀ (K : Type u_4) {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  (x : L), (Algebra.trace K L) x = ↑(Module.finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
-- Mathlib.Topology.Spectral.Prespectral
instPrespectralSpaceOfNoetherianSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.NoetherianSpace X], PrespectralSpace X
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.HasBasis.filter_totallyBounded_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α},
  (uniformity α).HasBasis p U →
    ∀ {f : Filter α}, f.TotallyBounded ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ (U i).preimage t ∈ f
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.X₄ = sq.X₄
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_1.eq_2 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (h_1 : (goals' : List Lean.MVarId) → motive (some goals'))
  (h_2 : Unit → motive none),
  (match none with
    | some goals' => h_1 goals'
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Nat.Gcd
Nat.gcd.induction : ∀ {P : ℕ → ℕ → Prop} (m n : ℕ), (∀ (n : ℕ), P 0 n) → (∀ (m n : ℕ), 0 < m → P (n % m) m → P m n) → P m n