mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Continuity
/-- `continuity` solves goals of the form `Continuous f` by applying lemmas tagged with the attribute
`@[continuity]`. If the goal is not solved after attempting all rules, `continuity` fails.

`fun_prop` is a (usually more powerful) alternative to `continuity`.

This tactic is extensible. Tagging lemmas with the `@[continuity]` attribute can allow `continuity`
to solve more goals.

* `continuity?` reports the proof script found by `continuity`.
 -/
tacticContinuity? : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Orientation
Module.Basis.abs_det_adjustToOrientation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  [inst_7 : Nonempty ι] (e : Module.Basis ι R M) (x : Orientation R M ι) (v : ι → M),
  |(e.adjustToOrientation x).det v| = |e.det v|
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α}
  {h' : k ∈ Std.ExtDTreeMap.map f t}, (Std.ExtDTreeMap.map f t).get k h' = f k (t.get k ⋯)
-- Mathlib.Logic.Function.Basic
Function.Injective.of_comp_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (g : γ → α), Function.Injective (f ∘ g) ↔ Function.Injective g
-- Lean.Meta.Basic
/-- Runs `k x` with the local declaration `<name> : <type> := <val>` added to the local context, where `x` is the new free variable.
Afterwards, the result is wrapped in the given `let`/`have` expression (according to the value of `nondep`).
- If `usedLetOnly := true` (the default) then the `let`/`have` is not created if the variable is unused.
 -/
Lean.Meta.mapLetDecl : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      [MonadLiftT Lean.MetaM n] →
        Lean.Name →
          Lean.Expr →
            Lean.Expr →
              (Lean.Expr → n Lean.Expr) →
                optParam Bool false →
                  optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → optParam Bool true → n Lean.Expr
-- Lean.Meta.Instances
Lean.Meta.addInstance : Lean.Name → Lean.AttributeKind → ℕ → Lean.MetaM Unit
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo : Type
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.comap_iSup : ∀ {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : α → β) (m : ι → MeasureTheory.OuterMeasure β),
  (MeasureTheory.OuterMeasure.comap f) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.comap f) (m i)
-- Mathlib.Combinatorics.SimpleGraph.Tutte
SimpleGraph.deleteUniversalVerts.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V), G.deleteUniversalVerts = ⊤.deleteVerts G.universalVerts
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, a ∈ m
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : Mul M],
  SimpleGraph.mulCayley s = SimpleGraph.fromRel fun x1 x2 => ∃ g ∈ s, x1 * g = x2
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.mk : Lean.Widget.InteractiveGoalCore →
  Option String → String → Lean.MVarId → Option Bool → Option Bool → Lean.Widget.InteractiveGoal
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instMonoidWithZero : {α : Type u_1} →
  [DecidableEq α] → [inst : MonoidWithZero α] → [NoZeroDivisors α] → [Nontrivial α] → MonoidWithZero (WithTop α)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.nat_of_atTop : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {f : ℕ → E''}
  {g : ℕ → F''}, f =O[Filter.atTop] g → ∀ {l : Filter ℕ}, (∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0) → f =O[l] g
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The distance from the circumcenter to the reflection of the orthocenter in a side equals the
circumradius, variant using a `Finset`.  -/
Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ : Fin 3},
  i₁ ≠ i₂ →
    dist (Affine.Simplex.circumcenter t)
        ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) t.orthocenter) =
      Affine.Simplex.circumradius t
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.objEquiv_apply : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (a : C),
  (CategoryTheory.Localization.Construction.objEquiv W) a = W.Q.obj a
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioo_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioo a.succ b.succ, f i = ∏ i ∈ Finset.Ioo a b, f i.succ
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening of a set contains the closure of the set.  -/
Metric.closure_subset_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, 0 < δ → ∀ (E : Set α), closure E ⊆ Metric.thickening δ E
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a}, t.isEmpty = true → t.getD a fallback = fallback
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.complOrderIso_apply : ∀ (α : Type u_2) [inst : TopologicalSpace α] (a : TopologicalSpace.Closeds α),
  (TopologicalSpace.Closeds.complOrderIso α) a = (⇑OrderDual.toDual ∘ TopologicalSpace.Closeds.compl) a
-- Std.Time.Internal.Bounded
/-- Adds one to the value of the bounded if the value is less than the higher bound of the bounded number.
 -/
Std.Time.Internal.Bounded.LE.succ : {lo hi : ℤ} → (bounded : Std.Time.Internal.Bounded.LE lo hi) → ↑bounded < hi → Std.Time.Internal.Bounded.LE lo hi
-- Init.Data.Option.Array
Option.toArray_bind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β},
  (o.bind f).toArray = Array.flatMap (Option.toArray ∘ f) o.toArray
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 2 (α × β)), ‖x‖ = √(‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.rec.eq_1 : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F α → α), QPF.Fix.rec g = Quot.lift (QPF.recF g) ⋯
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeRight_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : AddZeroClass H] (f : Additive G ≃+ H)
  (a : Multiplicative H),
  (AddEquiv.toMultiplicativeRight f).symm a = (AddMonoidHom.toMultiplicativeLeft f.symm.toAddMonoidHom) a
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.rev : Option Lean.Grind.AC.Seq → Option Lean.Grind.AC.Seq
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Returns true if the given predicate is true for any item in the RBMap.  -/
RBTree.RBMap.any : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → (α → β → Bool) → Bool
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.MatchResult.undecided.sizeOf_spec : sizeOf Lean.Elab.Term.Quotation.MatchResult.undecided = 1
-- Mathlib.RingTheory.FinitePresentation
RingHom.FiniteType.of_finitePresentation : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.FinitePresentation → f.FiniteType
-- Init.Data.List.Lex
List.nil_lex_cons' : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {l : List α}, List.Lex r [] (a :: l)
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhds_ne_bot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_mul_cexp_neg_mul_sq : ∀ {b : ℂ}, 0 < b.re → MeasureTheory.Integrable (fun x => ↑x * Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.preimageEquivFiber_apply_asIdeal : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p})),
  ((PrimeSpectrum.preimageEquivFiber R S p) q).asIdeal =
    RingHom.ker
      (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_add : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    I ^ n = 0 →
      ∀ {m : ℕ} {x : A},
        x ∈ I →
          ∀ {y : A},
            y ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (x + y) =
                ∑ k ∈ Finset.HasAntidiagonal.antidiagonal m,
                  DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_keyAtIdx? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] {t : Std.DTreeMap.Internal.Impl α β} {i : ℕ},
  t.keyAtIdx! i = (t.keyAtIdx? i).get!
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.nterm : Lean.Expr → Lean.Expr × ℤ → ℕ × Lean.Expr → Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.RingTheory.Finiteness.Basic
/-- If a module is finite over a linearly ordered ring, then it is also finite over the non-negative
scalars.  -/
instModuleFinite : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [Module.Finite R E], Module.Finite { c // 0 ≤ c } E
-- Mathlib.GroupTheory.Nilpotent
AddGroup.nilpotencyClass_zero_iff_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.IsNilpotent G], AddGroup.nilpotencyClass G = 0 ↔ Subsingleton G
-- Mathlib.RingTheory.Nilpotent.Basic
not_isNilpotent_neg_one : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R], ¬IsNilpotent (-1)
-- Mathlib.Data.Finset.Option
Option.mem_toFinset : ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ o.toFinset ↔ a ∈ o
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.instIsEquivalenceMapOfIsIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} [CategoryTheory.IsIso f],
  (CategoryTheory.Over.map f).IsEquivalence
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.isTrail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v), (↑p).IsTrail
-- Mathlib.Algebra.Homology.HomologySequence
/-- If `0 ⟶ X₁ ⟶ X₂ ⟶ X₃` is an exact sequence of homological complex, then
`0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i` is exact. This lemma states
the exactness at `X₂.cycles i`, while the fact that `X₁.cycles i ⟶ X₂.cycles i`
is a mono is an instance.  -/
HomologicalComplex.cycles_left_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.Exact →
    ∀ [CategoryTheory.Mono S.f] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
      [inst_5 : S.X₃.HasHomology i],
      { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := HomologicalComplex.cyclesMap S.f i,
          g := HomologicalComplex.cyclesMap S.g i, zero := ⋯ }.Exact
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf : ∀ {α : Type u} [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → ∀ (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt.eq_zero_iff : ∀ {p : ℕ} {z : ℤ}, padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬↑p ∣ z
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `monovaryOn_iff_exists_antitoneOn`. -/
MonovaryOn.exists_antitoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → ∃ x, AntitoneOn f s ∧ AntitoneOn g s
-- Mathlib.Data.Matrix.Mul
Matrix.neg_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : HasDistribNeg α] (w : m → α) (v : n → α),
  Matrix.vecMulVec (-w) v = -Matrix.vecMulVec w v
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.refl_trans : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), (Diffeomorph.refl I M n).trans h = h
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_le_aleph_one : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c ≤ Cardinal.aleph 1 ↔ c ≤ Cardinal.aleph 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.span_iUnion : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (s : ι → Set M),
  LieSubmodule.lieSpan R L (⋃ i, s i) = ⨆ i, LieSubmodule.lieSpan R L (s i)
-- Mathlib.Algebra.Star.LinearMap
/-- The intrinsic star operation on linear maps `E →ₗ F` defined by
`(star f) x = star (f (star x))`.  -/
LinearMap.intrinsicStar : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] → [inst_8 : StarAddMonoid F] → [StarModule R F] → Star (WithConv (E →ₗ[R] F))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_mono : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {f : G →g G'} {H₁ H₂ : G.Subgraph},
  H₁ ≤ H₂ → SimpleGraph.Subgraph.map f H₁ ≤ SimpleGraph.Subgraph.map f H₂
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_var : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (x : Lean.Grind.AC.Var),
  Lean.Grind.AC.Seq.denote ctx (Lean.Grind.AC.Seq.var x) = Lean.Grind.AC.Var.denote ctx x
-- Mathlib.Algebra.Ring.Prod
/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `R`.  -/
RingHom.fst : (R : Type u_1) → (S : Type u_3) → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R × S →+* R
-- Mathlib.Tactic.Translate.Core
/-- No argument needs to be checked. This is specified with `(relevant_arg := _)`.  -/
Mathlib.Tactic.Translate.RelevantArg.noArg : Mathlib.Tactic.Translate.RelevantArg
-- Init.Data.SInt.Lemmas
Int64.toInt_toInt16 : ∀ (x : Int64), x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
-- Mathlib.Data.Nat.Fib.Basic
Nat.gcd_fib_add_mul_self : ∀ (m n k : ℕ), (Nat.fib m).gcd (Nat.fib (n + k * m)) = (Nat.fib m).gcd (Nat.fib n)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- A typeclass for `SMul` structures which can be moved across a tensor product.

This typeclass is generated automatically from an `IsScalarTower` instance, but exists so that
we can also add an instance for `AddCommGroup.toIntModule`, allowing `z •` to be moved even if
`R` does not support negation.

Note that `Module R' (M ⊗[R] N)` is available even without this typeclass on `R'`; it's only
needed if `TensorProduct.smul_tmul`, `TensorProduct.smul_tmul'`, or `TensorProduct.tmul_smul` is
used.
 -/
TensorProduct.CompatibleSMul : (R : Type u_1) →
  (R' : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : Monoid R'] →
        (M : Type u_7) →
          (N : Type u_8) →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [DistribMulAction R' M] → [Module R M] → [Module R N] → [DistribMulAction R' N] → Prop
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.mk : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    [inst_1 : LE α] → (toClopens : TopologicalSpace.Clopens α) → IsUpperSet toClopens.carrier → ClopenUpperSet α
-- Init.Data.Nat.Lemmas
Nat.two_pow_pred_lt_two_pow : ∀ {w : ℕ}, 0 < w → 2 ^ (w - 1) < 2 ^ w
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.pointReflection_involutive : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x : P₁), Function.Involutive ⇑(AffineEquiv.pointReflection k x)
-- Mathlib.Data.Int.Cast.Basic
Int.cast_two : ∀ {R : Type u} [inst : AddGroupWithOne R], ↑2 = 2
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_mul' : ∀ {R' : Type u_5} {E : Type u_6} [inst : CommSemiring R'] [inst_1 : StarRing R'] [inst_2 : NonUnitalNonAssocSemiring E]
  [inst_3 : StarRing E] [inst_4 : Module R' E] [inst_5 : StarModule R' E] [inst_6 : SMulCommClass R' E E]
  [inst_7 : IsScalarTower R' E E],
  star (WithConv.toConv (LinearMap.mul' R' E)) = WithConv.toConv (LinearMap.mul' R' E ∘ₗ ↑(TensorProduct.comm R' E E))
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP'.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (l l_1 : FreeMonoid α),
      l = l_1 → FreeMonoid.countP' p l = FreeMonoid.countP' p_1 l_1
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableOn_coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_13 : MemTrivializationAtlas e]
  [inst_14 : MemTrivializationAtlas e'] [inst_15 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB],
  MDiff[e.baseSet ∩ e'.baseSet] fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.balRight_toList : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  (l.balRight v r).toList = l.toList ++ v :: r.toList
-- Mathlib.Order.Defs.PartialOrder
lt_iff_le_not_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Init.Data.BitVec.Lemmas
BitVec.toInt_nonneg_of_msb_false : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → 0 ≤ x.toInt
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopEquivalence_functor : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.unopEquivalence V c).functor = HomologicalComplex.unopFunctor V c
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatLe : Int.Internal.Linear.Poly → Bool
-- Lean.Environment
Lean.PersistentEnvExtension.toEnvExtension : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_neg : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G], IsOpenMap Neg.neg
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.one_mem_coeffSubmodule : ∀ {R₀ : Type u_1} {R : Type u_2} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] {n : ℕ}
  {e : ChevalleyThm.PolynomialC.InductionObj✝ R n}, 1 ∈ ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀ e
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyFlat.cofiltered : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.RepresentablyFlat F] (X : D),
  CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X F)
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.rowStochastic.eq_1 : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R],
  Matrix.rowStochastic R n =
    { carrier := {M | (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (k : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k.hom) g.arrow = f.arrow
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.instSMulCommClassMulOppositeSubtypeMem : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), SMulCommClass R Rᵐᵒᵖ ↥I
-- Mathlib.Order.Height
Set.chainHeight_eq_iSup : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r = ⨆ t, (↑t).encard
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  Quaternion.normSq a = 0 ↔ a = 0
-- Batteries.Data.List.Lemmas
List.disjoint_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₂ → a ∉ l₁
-- Lean.Parser.Command
Lean.Parser.Command.coinductive.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Prelude
/-- The underlying type of a `NonemptyType`.  -/
NonemptyType.type : NonemptyType → Type u
-- Mathlib.Algebra.Torsor.Basic
Set.singleton_vsub_self : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), {p} -ᵥ {p} = {0}
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- A module `M` over a commutative ring `R` is *faithfully flat* if it is flat and,
for all `R`-linear maps `f : N → N'` such that `id ⊗ f = 0`, we have `f = 0`.
 -/
Module.FaithfullyFlat : (R : Type u) → (M : Type v) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instAddAction.eq_1 : ∀ {M : Type u_3} {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α],
  AddUnits.instAddAction = { toVAdd := AddUnits.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Topology.MetricSpace.BundledFun
/-- A pseudometric must take identical elements to 0.  -/
PseudoMetric.refl' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (self : PseudoMetric X R) (x : X),
  self.toFun x x = 0
-- Mathlib.RingTheory.Ideal.Over
Ideal.ne_bot_of_liesOver_of_ne_bot : ∀ {A : Type u_2} {B : Type u_3} [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : Algebra A B] [FaithfulSMul A B]
  {p : Ideal A}, p ≠ ⊥ → ∀ (P : Ideal B) [P.LiesOver p], P ≠ ⊥
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_mod : ∀ (a : ℤ) (b : ℕ), ↑(a % ↑b) = ↑a
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def' : ∀ {α : Type u_1} (f : α → ℚ → ℝ) (a : α),
  ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a = fun t => ⨅ r, f a ↑r
-- Init.Prelude
MonadWithReaderOf.mk : {ρ : semiOutParam (Type u)} → {m : Type u → Type v} → ({α : Type u} → (ρ → ρ) → m α → m α) → MonadWithReaderOf ρ m
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.instDecidableRelAdjStarGraphOfDecidableEq : {V : Type u_1} → [DecidableEq V] → (r : V) → DecidableRel (SimpleGraph.starGraph r).Adj