mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getSuccessProbability : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m Aesop.Percent
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.inverse_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : N), (f.inverse g h₁ h₂) a = g a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The connecting homomorphism `(t.truncGT n).obj X ⟶ ((t.truncLE n).obj X)⟦1⟧`
for `n : ℤ`, as a natural transformation.  -/
CategoryTheory.Triangulated.TStructure.truncGTδLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (n : ℤ) → t.truncGT n ⟶ (t.truncLE n).comp (CategoryTheory.shiftFunctor C 1)
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_pos_of_exponent_pos : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α],
  0 < Monoid.exponent M → ∀ (m : M) (a : α), 0 < MulAction.period m a
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneraciesVanish_succ_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} (f : X.obj (Opposite.op { len := n + 1 }) ⟶ T),
  AlgebraicTopology.DoldKan.DegeneraciesVanish f ↔ ∀ (i : Fin (n + 1)), CategoryTheory.CategoryStruct.comp (X.σ i) f = 0
-- Std.Time.Zoned.TimeZone
Std.Time.instDecidableEqTimeZone : DecidableEq Std.Time.TimeZone
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_mul : ∀ {a b : ENNReal}, a ≠ 0 ∨ b ≠ ⊤ → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : Zero R], (↑x).imJ = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_eq_measure_of_between_null_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedRing.toPseudoMetricSpace : {α : Type u_5} → [self : SeminormedRing α] → PseudoMetricSpace α
-- Mathlib.Analysis.Normed.Group.Uniform
MonoidHomClass.antilipschitz_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal},
  (∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.addThms? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.Algebra.Group.Submonoid.Defs
AddMonoidHom.mem_eqLocusM : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N} {x : M},
  x ∈ f.eqLocusM g ↔ f x = g x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- The canonical isomorphism from the opposite of the binary product to the coproduct in the opposite
category.
 -/
CategoryTheory.Limits.opProdIsoCoprod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (A B : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] → Opposite.op (A ⨯ B) ≅ Opposite.op A ⨿ Opposite.op B
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
RingCon.ker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (f : M →+* N),
  RingCon.ker f = ⊥.comap f
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_mul : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ},
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsInt a a' →
      Mathlib.Meta.NormNum.IsInt b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsInt (a * b) c
-- Lean.Meta.Tactic.Induction
/-- Auxiliary method for implementing `induction`-like tactics.
It retrieves indices from `majorType` using `recursorInfo`.
Remark: `mvarId` and `tacticName` are used to generate error messages.
 -/
Lean.Meta.getMajorTypeIndices : Lean.MVarId → Lean.Name → Lean.Meta.RecursorInfo → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Algebra.Module.End
Module.toAddMonoidEnd_apply_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : R) (x_1 : M),
  ((Module.toAddMonoidEnd R M) x) x_1 = x • x_1
-- Mathlib.Data.Finset.Defs
Finset.ext : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, (∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact : ∀ {α : Type u_2} [inst : TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)},
  TopologicalSpace.Opens.IsBasis B →
    ∀ {U : TopologicalSpace.Opens α}, IsCompact U.carrier → ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
-- Mathlib.Analysis.Complex.Harmonic.Poisson
/-- **Poisson integral formula** for harmonic functions on arbitrary disks in the complex plane,
formulated with the Poisson kernel of integration.
 -/
InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul : ∀ {f : ℂ → ℝ} {c w : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R) →
    w ∈ Metric.ball c R → Real.circleAverage (poissonKernel c w • f) c R = f w
-- Mathlib.Logic.Basic
imp_or' : ∀ {a : Sort u_1} {b c : Prop}, (∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c
-- Mathlib.Tactic.Simps.Basic
/-- Projection data for a single projection of a structure  -/
Simps.ProjectionData : Type
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points lie in the affine span of two points, the first three points are collinear.  -/
collinear_triple_of_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ p₅ : P},
  p₁ ∈ line[k, p₄, p₅] → p₂ ∈ line[k, p₄, p₅] → p₃ ∈ line[k, p₄, p₅] → Collinear k {p₁, p₂, p₃}
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.fun_sum : ∀ {𝕜 : 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] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F} {A' : ι → E →L[𝕜] F},
  (∀ i ∈ u, HasFDerivAt (A i) (A' i) x) → HasFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
-- Mathlib.Data.Sigma.Order
/-- The lexicographical linear order on a sigma type.  -/
Sigma.Lex.orderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : PartialOrder ι] →
      [inst_1 : OrderBot ι] → [inst_2 : (i : ι) → Preorder (α i)] → [OrderBot (α ⊥)] → OrderBot (Σₗ (i : ι), α i)
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is regular if and only if `R` is trivial.  -/
IsRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRegular 0 → Subsingleton R
-- Mathlib.Data.Sign.Basic
SignType.zpow_even : ∀ (s : SignType) {z : ℤ}, Even z → s ≠ 0 → s ^ z = 1
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_derivation : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G), ⇑↑X = ⇑X
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
  [inst_2 : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)],
  (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).left = h₁
-- Mathlib.RepresentationTheory.Maschke
LinearMap.sumOfConjugatesEquivariant.congr_simp : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π π_1 : W →ₗ[k] V),
  π = π_1 →
    ∀ [inst_10 : Fintype G], LinearMap.sumOfConjugatesEquivariant G π = LinearMap.sumOfConjugatesEquivariant G π_1
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instNonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Nonempty (NonemptyInterval α)
-- Mathlib.Data.Stream.Init
/-- Alias for `Stream'.eta` to match `List` API.  -/
Stream'.cons_head_tail : ∀ {α : Type u} (s : Stream' α), Stream'.cons s.head s.tail = s
-- Init.Data.String.Basic
String.Pos.ne_startPos_of_lt : ∀ {s : String} {p q : s.Pos}, p < q → q ≠ s.startPos
-- Init.SimpLemmas
Bool.not_not : ∀ (b : Bool), (!!b) = b
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_eq_finrank_sub : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N},
  f.index = ↑(Module.finrank R ↥f.ker) - ↑(Module.finrank R (N ⧸ f.range))
-- Mathlib.Logic.Relation
/-- **Alias** of `refl`. -/
IsRefl.reflexive : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a
-- Mathlib.ModelTheory.Equivalence
/-- `φ ⟹[T] ψ` indicates that `φ` implies `ψ` in models of `T`.  -/
FirstOrder.«term_⟹[_]_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Baire.BaireMeasurable
/-- A set is Baire measurable if and only if it differs from some open set by a meager set.  -/
BaireMeasurableSet.iff_residualEq_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, BaireMeasurableSet s ↔ ∃ u, IsOpen u ∧ s =ᶠ[residual α] u
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The condition that a cochain complex `K` is strictly `≤ n`.  -/
CochainComplex.IsStrictlyLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CochainComplex C ℤ → ℤ → Prop
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatchAtChain_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain p pos pos' ↔
    pos ≤ pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h : pos'' < pos'), p (pos''.get ⋯) = true
-- Mathlib.RingTheory.QuotSMulTop
/-- An abbreviation for `M⧸rM` that keeps us from having to write
`(⊤ : Submodule R M)` over and over to satisfy the typechecker.  -/
QuotSMulTop : {R : Type u_2} → [inst : CommRing R] → R → (M : Type u_1) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_1
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_join : ∀ {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)), S.join.destruct = S.destruct.bind Stream'.WSeq.destruct_join.aux
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Equivalence between `Composition n` and `CompositionAsSet n`.  -/
compositionEquiv : (n : ℕ) → Composition n ≃ CompositionAsSet n
-- Mathlib.Topology.Convenient.Category
/-- the underlying `X`-continuous map of a morphism in `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.Hom.hom : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y Z : ContinuousGeneratedByCat X} → Y.Hom Z → Topology.ContinuousMapGeneratedBy X ↑Y ↑Z
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropPrefix?_eq_dropPrefix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.dropPrefix? pat = s.toSlice.dropPrefix? pat
-- Lean.DocString.Parser
/-- Disables the option `doc.verso` while running a parser.
 -/
Lean.Doc.Parser.withoutVersoSyntax : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_eq_top : ∀ {r : ENNReal}, ⌊r⌋ₑ = ⊤ ↔ r = ⊤
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.mk.inj : ∀ {α : Type u₁} {as as_1 : α}, { as := as } = { as := as_1 } → as = as_1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding the angles between two vectors in each order, with the second vector in each angle
negated, results in 0.  -/
Orientation.oangle_add_oangle_rev_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle x (-y) + o.oangle y (-x) = 0
-- Mathlib.ModelTheory.Syntax
/-- Relabels a bounded formula's variables along a particular function.  -/
FirstOrder.Language.BoundedFormula.relabel : {L : FirstOrder.Language} →
  {α : Type u'} →
    {β : Type v'} → {n : ℕ} → (α → β ⊕ Fin n) → {k : ℕ} → L.BoundedFormula α k → L.BoundedFormula β (n + k)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.stronglyAdapted : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0}, MeasureTheory.Martingale f ℱ μ → MeasureTheory.StronglyAdapted ℱ f
-- Init.Data.Order.Factories
/-- Returns a `LawfulOrderMax α` instance given that `max a b` returns either `a` or `b` and that
it is larger than or equal to both of them. The `≤` relation needs to be transitive.

The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
Std.LawfulOrderMax.of_le_max : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α]
  [i : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2],
  (∀ (a b : α), a ≤ a ⊔ b) →
    (∀ (a b : α), b ≤ a ⊔ b) →
      autoParam (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) Std.LawfulOrderMax.of_le_max._auto_1 → Std.LawfulOrderMax α
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2),
  (E.inter F).p₂ k =
    CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.p₁ k.1) (E.f i.1))
      (CategoryTheory.CategoryStruct.comp (F.p₁ k.2) (F.f i.2))
      (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd) (E.p₂ k.1) (F.p₂ k.2)
      (CategoryTheory.CategoryStruct.id S) ⋯ ⋯
-- Mathlib.Data.ENat.Pow
ENat.epow_add : ∀ {x y z : ℕ∞}, x ^ (y + z) = x ^ y * x ^ z
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_eq_toSlice_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String},
  s.dropEndWhile pat = s.toSlice ↔ s.endsWith pat = false
-- Mathlib.Combinatorics.Enumerative.Composition
/-- `index_exists` asserts there is some `i` with `j < c.sizeUpTo (i+1)`.
In the next definition `index` we use `Nat.find` to produce the minimal such index.
 -/
Composition.index_exists : ∀ {n : ℕ} (c : Composition n) {j : ℕ}, j < n → ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
-- Mathlib.Algebra.Group.Defs
MulOneClass.toMulOne : {M : Type u} → [self : MulOneClass M] → MulOne M
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_5 : ∀ (x : Turing.PartrecToTM2.Cont') (f g : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.trNormal (f.comp g) x = Turing.PartrecToTM2.trNormal g (Turing.PartrecToTM2.Cont'.comp f x)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.lhs_get_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α}
  (s : aig1.BinaryRefVec len) (idx : ℕ) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).lhs.get idx hidx = (s.lhs.get idx hidx).cast hcast
-- Mathlib.Topology.Algebra.UniformConvergence
instPowUniformFun : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [Pow β M] → Pow (UniformFun α β) M
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_add : ∀ {a b : ℤ} {hab₁ : ISize.minValue.toInt ≤ a + b} {hab₂ : a + b ≤ ISize.maxValue.toInt},
  ISize.ofIntLE (a + b) hab₁ hab₂ = ISize.ofInt a + ISize.ofInt b
-- Init.Data.BitVec.Lemmas
BitVec.toFin_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r : ℕ},
  (x.rotateLeft r).toFin = Fin.ofNat (2 ^ w) (x.toNat <<< (r % w)) ||| x.toFin / Fin.ofNat (2 ^ w) (2 ^ (w - r % w))
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_mono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty →
    ∀ {K₁ K₂ : TopologicalSpace.Compacts G},
      ↑K₁ ⊆ K₂.carrier →
        MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₁ ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₂
-- Std.Data.DTreeMap.Raw.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.DTreeMap.Raw.diff : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi`
for a version assuming `0 ≤ r` instead of `Nonempty β`.  -/
closedBall_pi' : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] [Nonempty β]
  (x : (b : β) → X b) (r : ℝ), Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
-- Lean.Util.Trace
/-- Similar to `withTraceNode`, but msg is constructed **before** executing `k`.
This is important when debugging methods such as `isDefEq`, and we want to generate the message
before `k` updates the metavariable assignment. The class `ExceptToTraceResult` is used to convert
the result produced by `k` into a `TraceResult` (success/failure/error), which is stored in
`TraceData.result?`. The rendering layer uses `TraceResult.toEmoji` to prepend the appropriate
emoji (✅️/❌️/💥️) when displaying the trace.

TODO: find better name for this function.
 -/
Lean.withTraceNodeBefore : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        {ε : Type} →
          [Lean.MonadRef m] →
            [Lean.AddMessageContext m] →
              [Lean.MonadOptions m] →
                [always : Lean.MonadAlwaysExcept ε m] →
                  [MonadLiftT BaseIO m] →
                    [Lean.ExceptToTraceResult ε α] →
                      Lean.Name → (Unit → m Lean.MessageData) → m α → optParam Bool true → optParam String "" → m α
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_5 : HAdd Std.Time.WallTime Std.Time.Millisecond.Offset Std.Time.WallTime
-- Mathlib.Topology.Order.LawsonTopology
/-- An upper set is Lawson open if and only if it is Scott open  -/
Topology.lawsonOpen_iff_scottOpen_of_isUpperSet : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  IsUpperSet s → (IsOpen (⇑Topology.WithLawson.ofLawson ⁻¹' s) ↔ IsOpen (⇑Topology.WithScott.ofScott ⁻¹' s))
-- Lean.CoreM
/-- Return `true` if diagnostic information collection is enabled.  -/
Lean.isDiagnosticsEnabled : Lean.CoreM Bool
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.congr_eq_4 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  x = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) ≍
      h_4 ()
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.comap_comap : ∀ {K : Type u} {L : Type v} {M : Type w} [inst : DivisionRing K] [inst_1 : DivisionRing L] [inst_2 : DivisionRing M]
  (s : Subfield M) (g : L →+* M) (f : K →+* L), Subfield.comap f (Subfield.comap g s) = Subfield.comap (g.comp f) s
-- Init.Data.List.Scan.Lemmas
List.getLast?_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β}, (List.scanr f b l).getLast? = some b
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.mapNatBool.congr_simp : ∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (x x_1 : α),
  x = x_1 → ∀ (n n_1 : ℕ), n = n_1 → MeasurableSpace.mapNatBool α x n = MeasurableSpace.mapNatBool α x_1 n_1
-- Mathlib.RingTheory.LocalRing.Basic
Field.instIsLocalRing : ∀ (K : Type u_3) [inst : Field K], IsLocalRing K
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.taylor_mem_degreeLT : ∀ {R : Type u_1} [inst : CommRing R] {r : R} {n : ℕ} {f : Polynomial R},
  (Polynomial.taylor r) f ∈ Polynomial.degreeLT R n ↔ f ∈ Polynomial.degreeLT R n
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- The derivations of a commutative Algebra themselves form a LieRinehart-Algebra.  -/
instLieRinehartAlgebraDerivation : ∀ {R : Type u_1} {A₁ : Type u_2} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : Algebra R A₁],
  LieRinehartAlgebra R A₁ (Derivation R A₁ A₁)
-- Init.PropLemmas
Decidable.not_or_of_imp : ∀ {a b : Prop} [Decidable a], (a → b) → ¬a ∨ b
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_filter_iff : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, m.WF → ((Std.HashSet.Raw.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false)
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.TreeMap.Raw.entryAtIdx! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → ℕ → α × β
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork
diagram of the Stacks entry.  -/
CategoryTheory.Presheaf.firstObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {U : C} → CategoryTheory.Presieve U → CategoryTheory.Functor Cᵒᵖ A → [CategoryTheory.Limits.HasProducts A] → A
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.nndist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → ∀ (x y : X), nndist (f x) (f y) ≤ C * nndist x y ^ ↑r
-- Mathlib.Algebra.Quandle
Rack.self_distrib_inv : ∀ {R : Type u_1} [inst : Rack R] {x y z : R},
  Rack.invAct x (Rack.invAct y z) = Rack.invAct (Rack.invAct x y) (Rack.invAct x z)