mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.ext : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  ⦃f g : L.Embedding M N⦄, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Order.UpperLower.Closure
UpperSet.coe_sdiff : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (t : Set α), ↑(s.sdiff t) = ↑s \ ↑(lowerClosure t)
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `Ord` across an `Equiv`.  -/
Equiv.ord : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Ord β] → Ord α
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.Functor.instPreservesEpimorphisms : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [inst_6 : F.PreservesZeroMorphisms]
  [F.PreservesHomology], F.PreservesEpimorphisms
-- Init.Data.List.Nat.Count
List.le_count_tail : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l - 1 ≤ List.count a l.tail
-- Init.Meta.Defs
Lean.Syntax.isNone : Lean.Syntax → Bool
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ ≠ p₂ ∨ p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.all_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {p : α → Bool},
  t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ext_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v w : MeasureTheory.VectorMeasure α M), v = w ↔ ∀ (i : Set α), MeasurableSet i → v i = w i
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  CategoryTheory.Presieve.IsSheafFor F E.presieve₀ →
    (∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j),
        CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) →
          CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows) →
      E.IsStronglySheafFor F
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.isUpper_orderDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α], Topology.IsUpper αᵒᵈ ↔ Topology.IsLower α
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_incl : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3)
  [inst_5 : CommRing R] [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L],
  ⇑(L'.incl R).toLieHom = Subtype.val
-- Mathlib.Data.Matrix.Basic
RingEquiv.mapMatrix_apply : ∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] (f : α ≃+* β) (M : Matrix m m α), f.mapMatrix M = M.map ⇑f
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → q ∈ as → dist q s.center ^ 2 = s.radius ^ 2 + dist q p ^ 2
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C)
  (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (F.comp G).mapComp f g = CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)) (G.map₂ (F.mapComp f g))
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Ico : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : LinearOrder X] [ClosedIciTopology X],
  IsLocallyClosed (Set.Ico a b)
-- Lean.Environment
Lean.instBEqConstantKind : BEq Lean.ConstantKind
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eval_map_algebraMap : ∀ {R : Type u} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B] (P : Polynomial R)
  (b : B), Polynomial.eval b (Polynomial.map (algebraMap R B) P) = (Polynomial.aeval b) P
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeatTR.loop.eq_1 : ∀ {α : Type u} (f : α → α) (x : α), Nat.repeatTR.loop✝ f 0 x = x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Proofs are ignored during E-matching. Lean is proof irrelevant.  -/
Lean.Meta.Grind.NormalizePattern.PatternArgKind.proof : Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two vectors, divided by the product of their
norms, has absolute value 1 if and only if they are nonzero and one is
a multiple of the other. One form of equality case for Cauchy-Schwarz.  -/
norm_inner_div_norm_mul_norm_eq_one_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖inner 𝕜 x y / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
-- Mathlib.Analysis.Convex.Quasiconvex
Convex.quasiconvexOn_restrict : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} [inst_4 : Preorder β] {s : Set E} {f : E → β} {t : Set E},
  QuasiconvexOn 𝕜 s f → t ⊆ s → Convex 𝕜 t → QuasiconvexOn 𝕜 t f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.coe_eq_bot_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (Q : AffineSubspace k P), ↑Q = ∅ ↔ Q = ⊥
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.toIsNormalEpiCategory : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.IsNormalEpiCategory C
-- Init.Grind.Tactics
/-- `grind_linarith` solves simple goals about linear arithmetic.

It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `linarith` solver.
Please use `grind` instead if you need additional capabilities.
 -/
Lean.Parser.Tactic.grind_linarith : Lean.ParserDescr
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_ofNat : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : NatCast R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], (HahnSeries.single 0) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_eq_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ),
  e.transPartialEquiv f' = e.toPartialEquiv.trans f'
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Config.mk.sizeOf_spec : ∀ (red : Lean.Meta.TransparencyMode) (zetaDelta contextual : Bool),
  sizeOf { red := red, zetaDelta := zetaDelta, contextual := contextual } =
    1 + sizeOf red + sizeOf zetaDelta + sizeOf contextual
-- Init.Data.Nat.Fold
Nat.dfoldRev_add : ∀ {n m : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + m) Nat.dfoldRev_add._auto_5 → Type u}
  (f : (i : ℕ) → (h : i < n + m) → α (i + 1) ⋯ → α i ⋯) (init : α (n + m) ⋯),
  (n + m).dfoldRev f init = n.dfoldRev (fun i h => f i ⋯) (m.dfoldRev (fun i h => f (n + i) ⋯) init)
-- Mathlib.GroupTheory.QuotientGroup.Defs
Con.mem_subgroup_iff : ∀ {G : Type u_1} [inst : Group G] {c : Con G} {x : G}, x ∈ c.subgroup ↔ c x 1
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_mono : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R], Monotone Nat.ceil
-- Mathlib.Data.Num.ZNum
ZNum.cast_neg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : PosNum), ↑(ZNum.neg n) = -↑n
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.ngen : Lean.Meta.AbstractMVars.State → Lean.NameGenerator
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.isBigO_sub : ∀ {𝕜 : 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}
  {x₀ : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x₀ → (fun x => f x - f x₀) =O[nhdsWithin x₀ s] fun x => x - x₀
-- Mathlib.GroupTheory.Torsion
/-- Elements of the `p`-primary component have additive order `p^n` for some `n`.  -/
AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul : ∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(AddCommMonoid.primaryComponent G p)),
  ∃ n, addOrderOf g = p ^ n
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.instEpiGL₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Epi S.L₀'.g
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) →
          (x : Turing.TM2.Stmt Γ Λ σ) →
            ((k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q)) →
              ((k : K) →
                  (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q)) →
                ((k : K) →
                    (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q)) →
                  ((a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q)) →
                    ((a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂)) →
                      ((a : σ → Λ) → motive (Turing.TM2.Stmt.goto a)) → (Unit → motive Turing.TM2.Stmt.halt) → motive x
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.lt_ord : ∀ {c : Cardinal.{u_1}} {o : Ordinal.{u_1}}, o < c.ord ↔ o.card < c
-- Mathlib.Data.Nat.Set
Nat.range_rec : ∀ {α : Type u_2} (x : α) (f : ℕ → α → α),
  (Set.range fun n => Nat.rec x f n) = {x} ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ Nat.succ) n
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.principal_σ : ∀ {α : Type u_1} (s : Set α), (Filter.Realizer.principal s).σ = Unit
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Submodule.toNonUnitalSubalgebra_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (p : Submodule R A) (hmul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p),
  p.toNonUnitalSubalgebra hmul = { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.image_out : ∀ {V : Type u} {G : SimpleGraph V} (C : Set G.ConnectedComponent),
  SimpleGraph.ConnectedComponent.Represents (Quot.out '' C) C
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The colimit of `F.leftOp` is the unopposite of `limit F`.  -/
CategoryTheory.Limits.colimitLeftOpIsoUnopLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.colimit F.leftOp ≅ Opposite.unop (CategoryTheory.Limits.limit F)
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (a : 𝕜), RCLike.sqrt a = (RCLike.map ℂ 𝕜) ((RCLike.map 𝕜 ℂ) a).sqrt
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isBounded_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ {s : Set β}, Bornology.IsBounded s → Bornology.IsBounded (f ⁻¹' s)
-- Init.Data.List.Lemmas
List.foldr.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β → β) (init : β), List.foldr f init [] = init
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.mk.sizeOf_spec : ∀ (alt : String) (name : Lean.StrLit), sizeOf { alt := alt, name := name } = 1 + sizeOf alt + sizeOf name
-- Mathlib.Analysis.Normed.Module.Bases
/-- The dimension of the range of the projection `proj A` equals the cardinality of `A`.  -/
GeneralSchauderBasis.finrank_range_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L) (A : Finset β),
  Module.finrank 𝕜 ↥(↑(b.proj A)).range = A.card
-- Mathlib.Data.NNRat.Defs
NNRat.ne_iff : ∀ {x y : ℚ≥0}, ↑x ≠ ↑y ↔ x ≠ y
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.instFaithfulOfIsThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [Quiver.IsThin C], F.Faithful
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore.inj : ∀ {e : Lean.Expr} {lhs rhs : Lean.Grind.CommRing.Expr} {e_1 : Lean.Expr} {lhs_1 rhs_1 : Lean.Grind.CommRing.Expr},
  Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore e_1 lhs_1 rhs_1 →
    e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Counterpart to `List.prod_take_succ` when we have an inverse operation  -/
List.prod_drop_succ : ∀ {G : Type u_7} [inst : Group G] (L : List G) (i : ℕ) (p : i < L.length),
  (List.drop (i + 1) L).prod = L[i]⁻¹ * (List.drop i L).prod
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.div_two_le_of_lt_two : ∀ {m n : ℕ}, m < 2 ^ n.succ → m / 2 < 2 ^ n
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mk.inj : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {toSubmodule : Submodule R L}
  {lie_mem' : ∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier}
  {toSubmodule_1 : Submodule R L}
  {lie_mem'_1 : ∀ {x y : L}, x ∈ toSubmodule_1.carrier → y ∈ toSubmodule_1.carrier → ⁅x, y⁆ ∈ toSubmodule_1.carrier},
  { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := lie_mem'_1 } →
    toSubmodule = toSubmodule_1
-- Mathlib.CategoryTheory.EssentiallySmall
/-- The categorical equivalence between `C` and `ShrinkHoms C`, when `C` is locally small.
 -/
CategoryTheory.ShrinkHoms.equivalence : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] → C ≌ CategoryTheory.ShrinkHoms.{u} C
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.mk.inj : ∀ {argPos targetPos : ℕ} {motive : Option Lean.MVarId} {f fType : Lean.Expr} {alts : Array Lean.Elab.Tactic.ElimApp.Alt}
  {insts : Array Lean.MVarId} {argPos_1 targetPos_1 : ℕ} {motive_1 : Option Lean.MVarId} {f_1 fType_1 : Lean.Expr}
  {alts_1 : Array Lean.Elab.Tactic.ElimApp.Alt} {insts_1 : Array Lean.MVarId},
  { argPos := argPos, targetPos := targetPos, motive := motive, f := f, fType := fType, alts := alts, insts := insts } =
      { argPos := argPos_1, targetPos := targetPos_1, motive := motive_1, f := f_1, fType := fType_1, alts := alts_1,
        insts := insts_1 } →
    argPos = argPos_1 ∧
      targetPos = targetPos_1 ∧ motive = motive_1 ∧ f = f_1 ∧ fType = fType_1 ∧ alts = alts_1 ∧ insts = insts_1
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_iff : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, y ∈ PiNat.cylinder x n ↔ ∀ i < n, y i = x i
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_iff_infinite_of_nonneg : ∀ {x : ℝ*}, 0 ≤ x → (x.InfinitePos ↔ x.Infinite)
-- Qq.Typ
Qq.instCoeOutQuotedMessageData : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Topology.Hom.Open
/-- Copy of a `ContinuousOpenMap` with a new `ContinuousMap` equal to the old one. Useful to fix
definitional equalities.  -/
ContinuousOpenMap.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (f : α →CO β) → (f' : α → β) → f' = ⇑f → α →CO β
-- Mathlib.Order.BoundedOrder.Lattice
min_top_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] (a : α), min ⊤ a = a
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [toAlgebra : Algebra R A] →
          [toCoalgebra : Coalgebra R A] →
            CoalgebraStruct.counit 1 = 1 →
              (LinearMap.mul R A).compr₂ CoalgebraStruct.counit =
                  (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit →
                CoalgebraStruct.comul 1 = 1 →
                  (LinearMap.mul R A).compr₂ CoalgebraStruct.comul =
                      (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul →
                    Bialgebra R A
-- Std.Data.DTreeMap.Internal.Operations
/-- Removes the mapping with key `k`, if it exists.  -/
Std.DTreeMap.Internal.Impl.erase : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      α →
        (t : Std.DTreeMap.Internal.Impl α β) →
          t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (t.size - 1) t.size
-- Mathlib.Data.Finset.Max
Finset.max'_union : ∀ {α : Type u_2} [inst : LinearOrder α] {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty),
  (s₁ ∪ s₂).max' ⋯ = max (s₁.max' h₁) (s₂.max' h₂)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Semigroup M],
  MonoidAlgebra.nonUnitalSemiring =
    { toNonUnitalNonAssocSemiring := MonoidAlgebra.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.mk : Lean.Meta.Sym.SharedExprs → Lean.Meta.Sym.Config → Lean.Meta.Sym.Context
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_rco : ∀ {a b : ℕ}, (a...b).size = b - a
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ T₂ : CategoryTheory.Monad C} →
      (toNatTrans : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor) →
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
            CategoryTheory.MonadHom.app_η._autoParam →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
                  CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X)))
                    (T₂.μ.app X))
              CategoryTheory.MonadHom.app_μ._autoParam →
            CategoryTheory.MonadHom T₁ T₂
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- `AffineSubspace.shift s c r` can be represented by moving a point in the subspace
towards `c`.  -/
AffineSubspace.shift_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] {s : AffineSubspace k P} (p : ↥s) (c : P) (r : k),
  s.shift c r = AffineSubspace.map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑p)))) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The partial derivative `W_Y(X, Y, Z)` with respect to `Y` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in projective coordinates.  -/
WeierstrassCurve.Projective.polynomialY : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → MvPolynomial (Fin 3) R
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.subtype_apply : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {x : ↥S}, S.subtype x = ↑x
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk_le_mk : ∀ {G : Type u_1} [inst : AddGroup G] {s t : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier)
  (h_neg' : ∀ {x : G}, x ∈ t.carrier → -x ∈ t.carrier),
  { toAddSubmonoid := s, neg_mem' := h_neg } ≤ { toAddSubmonoid := t, neg_mem' := h_neg' } ↔ s ≤ t
-- Mathlib.Analysis.Complex.Exponential
Real.abs_exp_sub_one_sub_id_le : ∀ {x : ℝ}, |x| ≤ 1 → |Real.exp x - 1 - x| ≤ x ^ 2
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_mono : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a b : Associates.FactorSet α}, a ≤ b → a.prod ≤ b.prod
-- Init.Data.Vector.Monadic
Vector.mapM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : α → β} {g : β → m γ} {xs : Vector α n}, Vector.mapM g (Vector.map f xs) = Vector.mapM (g ∘ f) xs
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_piFinSuccAbove : ∀ {n : ℕ} (α : Fin (n + 1) → Type u) [inst : (i : Fin (n + 1)) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite MeasureTheory.volume] (i : Fin (n + 1)),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Tactic.FBinop
/-- Records a "functor", which is some function `Type u → Type v`. We only
allow `c a1 ... an` for `c` a constant. This is so we can abstract out the universe variables.  -/
FBinopElab.SRec : Type
-- Batteries.Data.List.Lemmas
List.mem_idxsOf_iff_exists_getElem_pos : ∀ {α : Type u_1} {xs : List α} {x : α} {i : ℕ} [inst : BEq α],
  i ∈ List.idxsOf x xs ↔ ∃ (hix : i < xs.length), (xs[i] == x) = true
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : BoundedOrder α] → Inhabited (BoundedOrderHom α α)
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.map_centralizer_le_centralizer_image : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (s : Set G) (f : G →* G'),
  Subgroup.map f (Subgroup.centralizer s) ≤ Subgroup.centralizer (⇑f '' s)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Subgroup.instCountableSubtypeMemZpowers : ∀ {G : Type u_1} [inst : Group G] (a : G), Countable ↥(Subgroup.zpowers a)
-- Mathlib.Order.Closure
ClosureOperator.ofPred.congr_simp : ∀ {α : Type u_1} [inst : PartialOrder α] (f f_1 : α → α) (e_f : f = f_1) (p p_1 : α → Prop) (e_p : p = p_1)
  (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y),
  ClosureOperator.ofPred f p hf hfp hmin = ClosureOperator.ofPred f_1 p_1 ⋯ ⋯ ⋯