mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar_mul : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] [inst_7 : MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [μ.IsAddHaarMeasure] [μ.Regular] (g : G) (s : Set A), ↑((MeasureTheory.distribHaarChar A) g) * μ s = μ (g • s)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ), e.leftOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.unop X)).op
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.norm_condExpInd_le : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  ‖MeasureTheory.condExpInd G hm μ s‖ ≤ μ.real s
-- Mathlib.CategoryTheory.GradedObject
/-- The `total` functor taking a graded object to the coproduct of its graded components is faithful.
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
which follows from the fact we have zero morphisms and decidable equality for the grading.
 -/
CategoryTheory.GradedObject.instFaithfulTotal : ∀ (β : Type) (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Limits.HasZeroMorphisms C], (CategoryTheory.GradedObject.total β C).Faithful
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instGeometricallyReducedMorphismRestrict : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (V : S.Opens) [AlgebraicGeometry.GeometricallyReduced f],
  AlgebraicGeometry.GeometricallyReduced (f ∣_ V)
-- Mathlib.Analysis.Normed.Ring.Int
Int.toNat_add_toNat_neg_eq_nnnorm : ∀ (n : ℤ), ↑n.toNat + ↑(-n).toNat = ‖n‖₊
-- Lean.Meta.Constructions.CtorElim
Lean.mkCtorElim : Lean.Name → Lean.MetaM Unit
-- Init.Core
Lean.Syntax.atom.injEq : ∀ (info : Lean.SourceInfo) (val : String) (info_1 : Lean.SourceInfo) (val_1 : String),
  (Lean.Syntax.atom info val = Lean.Syntax.atom info_1 val_1) = (info = info_1 ∧ val = val_1)
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
/-- `Equiv.mulLeft₀` as an order isomorphism.  -/
OrderIso.mulLeft₀ : {G₀ : Type u_1} →
  [inst : GroupWithZero G₀] → [inst_1 : PartialOrder G₀] → [PosMulReflectLT G₀] → (a : G₀) → 0 < a → G₀ ≃o G₀
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The nae of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.name : Mathlib.Tactic.ClickSuggestions.GrwKey → String
-- Init.Data.Int.Gcd
Int.lcm_ediv : ∀ {a b c : ℤ}, c ∣ a → c ∣ b → (a / c).lcm (b / c) = a.lcm b / c.natAbs
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.mk.inj : ∀ {β : Type u_4} {filter filter_1 : Filter (Finset β)},
  { filter := filter } = { filter := filter_1 } → filter = filter_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.erase_add_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : MonoidAlgebra R M),
  MonoidAlgebra.erase m x + MonoidAlgebra.single m (x.coeff m) = x
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_forall_le_5 : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ σ₅ : Type v} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → l},
  Lean.Order.PartialOrder.rel P Q ↔
    ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅),
      Lean.Order.PartialOrder.rel (P s₁ s₂ s₃ s₄ s₅) (Q s₁ s₂ s₃ s₄ s₅)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Int.padicValuation.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst : Fact (Nat.Prime p)], Int.padicValuation p = Int.padicValuation p_1
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toStarRing : {A : Type u_1} → [self : NonUnitalCStarAlgebra A] → StarRing A
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (x : ℤ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match 0, x with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc m, Int.ofNat n => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_1 x
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.xgcdAux_P : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R) {r r' s t s' t' : R},
  EuclideanDomain.P✝ a b (r, s, t) →
    EuclideanDomain.P✝ a b (r', s', t') → EuclideanDomain.P✝ a b (EuclideanDomain.xgcdAux r s t r' s' t')
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprDiscrInfo.repr : Lean.Meta.Match.DiscrInfo → ℕ → Std.Format
-- Mathlib.Topology.Compactness.CountablyCompact
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is countably compact if and
only if `s` is countably compact.  -/
Topology.IsInducing.isCountablyCompact_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F] {A : Set E} {f : E → F},
  Topology.IsInducing f → (IsCountablyCompact A ↔ IsCountablyCompact (f '' A))
-- Mathlib.RepresentationTheory.Basic
/-- Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$
(implemented by `dualTensorHom` in `Mathlib/LinearAlgebra/Contraction.lean`).
Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on
$Hom_k(V, W)$.
This lemma says that $φ$ is $G$-linear.
 -/
Representation.dualTensorHom_comm : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Group G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρV : Representation k G V) (ρW : Representation k G W) (g : G),
  dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.cokerπ_surjective : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N),
  Function.Surjective ⇑(TopModuleCat.Hom.hom (TopModuleCat.cokerπ φ))
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The precomposition of an homotopy class with a relative morphism.  -/
SSet.RelativeMorphism.HomotopyClass.precomp : {X Y Z : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {C : Z.Subcomplex} →
          {ψ : B.toSSet ⟶ C.toSSet} →
            SSet.RelativeMorphism.HomotopyClass B C ψ →
              SSet.RelativeMorphism A B φ →
                {φψ : A.toSSet ⟶ C.toSSet} →
                  CategoryTheory.CategoryStruct.comp φ ψ = φψ → SSet.RelativeMorphism.HomotopyClass A C φψ
-- Lean.Data.Lsp.Capabilities
/-- The latest RPC wire format supported by the client.
Defaults to `v0` when `none`.
 -/
Lean.Lsp.LeanClientCapabilities.rpcWireFormat? : Lean.Lsp.LeanClientCapabilities → Option Lean.Lsp.RpcWireFormat
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_sUnion : ∀ {V : Type u} {s : Set (Set (Sym2 V))}, SimpleGraph.fromEdgeSet (⋃₀ s) = sSup (SimpleGraph.fromEdgeSet '' s)
-- Mathlib.Algebra.Ring.Action.Submonoid
/-- The additive subgroup of elements fixed under the whole action.  -/
FixedPoints.addSubgroup : (M : Type u_1) → (α : Type u_2) → [inst : Monoid M] → [inst_1 : AddGroup α] → [DistribMulAction M α] → AddSubgroup α
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andLeft.injEq : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof) (ak_1 : Mathlib.Tactic.ITauto.AndKind)
  (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.andLeft ak p = Mathlib.Tactic.ITauto.Proof.andLeft ak_1 p_1) = (ak = ak_1 ∧ p = p_1)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Sum of a multiset of elements in an `IntermediateField` is in the `IntermediateField`.  -/
IntermediateField.multiset_sum_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (m : Multiset L), (∀ a ∈ m, a ∈ S) → m.sum ∈ S
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.one_notMem_supportAddSubgroup : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R), 1 ∉ P.supportAddSubgroup
-- Init.Core
instInhabitedProd : {α : Type u_1} → {β : Type u_2} → [Inhabited α] → [Inhabited β] → Inhabited (α × β)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {R : Type u_4} [inst_2 : Semiring R] [inst_3 : DistribMulAction R M] [inst_4 : ContinuousConstSMul R M]
  {v : MeasureTheory.VectorMeasure α M} {i : Set α} (c : R), (c • v).restrict i = c • v.restrict i
-- Plausible.Testable
Plausible.TestResult.failure.inj : ∀ {p : Prop} {a : ¬p} {a_1 : List String} {a_2 : ℕ} {a_3 : ¬p} {a_4 : List String} {a_5 : ℕ},
  Plausible.TestResult.failure a a_1 a_2 = Plausible.TestResult.failure a_3 a_4 a_5 → a_1 = a_4 ∧ a_2 = a_5
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.iterM_eq_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {array : Array β}, array.iterM m = array.iterFromIdxM m 0
-- Mathlib.Order.Category.Lat
Lat.mk.sizeOf_spec : ∀ (carrier : Type u_1) [str : Lattice carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_ineq_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.Group.Torsion
self_ne_neg : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {a : G}, a ≠ -a ↔ a ≠ 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₁_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (HomologicalComplex.cylinder.π K) =
    CategoryTheory.CategoryStruct.id K
-- Mathlib.Computability.Ackermann
/-- The Ackermann function is computable.  -/
computable₂_ack : Computable₂ ack
-- Mathlib.Probability.CondVar
/-- **Law of total variance**  -/
ProbabilityTheory.integral_condVar_add_variance_condExp : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  m ≤ m₀ →
    ∀ [MeasureTheory.IsProbabilityMeasure μ],
      MeasureTheory.MemLp X 2 μ →
        ∫ (x : Ω), ProbabilityTheory.condVar m X μ x ∂μ + ProbabilityTheory.variance μ[X | m] μ =
          ProbabilityTheory.variance X μ
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.flip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  P.IsOrthogonal i j → P.flip.IsOrthogonal i j
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.mk.injEq : ∀ (len len_1 : ℕ), ({ len := len } = { len := len_1 }) = (len = len_1)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.MemLp.essSup_norm_condExp_le_essSup_norm : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [NeZero μ] {f : α → E},
  MeasureTheory.MemLp f ⊤ μ → essSup (fun x => ‖μ[f | m] x‖) μ ≤ essSup (fun x => ‖f x‖) μ
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_set! : ∀ (data : ByteArray) (i : ℕ) (v : UInt8) (j : ℕ), i < data.size → (data.set! i v)[j]! = if i = j then v else data[j]!
-- Init.Data.Nat.Gcd
Nat.instCommutativeGcd : Std.Commutative Nat.gcd
-- Lean.Util.FindExpr
/-- Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application.  -/
Lean.Expr.findExt? : (Lean.Expr → Lean.Expr.FindStep) → Lean.Expr → Option Lean.Expr
-- Mathlib.Data.Fintype.EquivFin
/-- Noncomputable equivalence between a finset `s` as a fintype and `Fin n`, when there is a
proof that `#s = n`.  -/
Finset.equivFinOfCardEq : {α : Type u_1} → {s : Finset α} → {n : ℕ} → s.card = n → ↥s ≃ Fin n
-- ProofWidgets.Component.RefreshComponent
/-- An effectful wrapper around `Thunk.get` analogous to `IO.wait`.
Unlike `Thunk.get`, the compiler should never move this out of a `do` block.  -/
_private.ProofWidgets.Component.RefreshComponent.0.IO.forceThunk : {α : Type} → Thunk α → BaseIO α
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_add : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : ι → Set α) (t : Set α), (⋃ i, s i) + t = ⋃ i, s i + t
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.BisimO.match_1.eq_1 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (a a' : α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inl a, Sum.inl a' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_1 a a'
-- Std.Time.Date.PlainDate
/-- Determines the quarter of the year for the given `PlainDate`.
 -/
Std.Time.PlainDate.quarter : Std.Time.PlainDate → Std.Time.Internal.Bounded.LE 1 4
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The core TM1 → TM0 translation function. Here `s` is the current value on the tape, and the
`Stmt₁` is the TM1 statement to translate, with local state `v : σ`. We evaluate all regular
instructions recursively until we reach either a `move` or `write` command, or a `goto`; in the
latter case we emit a dummy `write s` step and transition to the new target location.  -/
Turing.TM1to0.trAux : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (M : Λ → Turing.TM1.Stmt Γ Λ σ) → Γ → Turing.TM1.Stmt Γ Λ σ → σ → Turing.TM1to0.Λ' M × Turing.TM0.Stmt Γ
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongr_one_swap : ∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : β),
  Equiv.Perm.sumCongr 1 (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.coe_iInf : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_4} (f : ι → AddCon M), ⇑(iInf f) = ⨅ i, ⇑(f i)
-- Lean.Parser.Term
/-- `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`.  -/
Lean.Parser.Term.matchDiscr : Lean.Parser.Parser
-- Mathlib.Topology.Order.IsLUB
DenseRange.exists_seq_strictAnti_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {β : Type u_3}
  [inst_3 : LinearOrder β] [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] {f : β → α},
  DenseRange f →
    Monotone f →
      ∀ (x : α), ∃ u, StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioi x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
-- Mathlib.Algebra.DirectSum.Internal
/-- The difference with `DirectSum.listProd_apply_eq_zero` is that the indices at which
the terms of the list are zero is allowed to vary.  -/
listProd_apply_eq_zero' : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [inst_4 : Semiring R] [inst_5 : SetLike σ R] [inst_6 : AddSubmonoidClass σ R] {A : ι → σ}
  [inst_7 : SetLike.GradedMonoid A] [CanonicallyOrderedAdd ι] {l : List ((DirectSum ι fun i => ↥(A i)) × ι)},
  (∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) → ∀ ⦃n : ι⦄, n < (List.map Prod.snd l).sum → (List.map Prod.fst l).prod n = 0
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.DefEqCacheKey.mk.injEq : ∀ (lhs rhs : Lean.Expr) (configKey : UInt64) (lhs_1 rhs_1 : Lean.Expr) (configKey_1 : UInt64),
  ({ lhs := lhs, rhs := rhs, configKey := configKey } = { lhs := lhs_1, rhs := rhs_1, configKey := configKey_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ configKey = configKey_1)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Composing on the left by a uniformly continuous function preserves uniform convergence  -/
UniformContinuousOn.comp_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] [inst_1 : UniformSpace γ]
  {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {g : β → γ},
  (∀ (i : ι) (x : α), F i x ∈ s) →
    (∀ (x : α), f x ∈ s) →
      UniformContinuousOn g s → TendstoUniformly F f p → TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ι_ofι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a)
  (w :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b))
  (i : J.L), (CategoryTheory.Limits.Multifork.ofι I P ι w).ι i = ι i
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `f : ⨁ S ⟶ ⨁ T` is an isomorphism, and `s` is a non-trivial summand of the source,
then there is some `t` in the target so that the `s, t` matrix entry of `f` is nonzero.
 -/
CategoryTheory.Biproduct.columnNonzeroOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {σ τ : Type} →
        [Fintype τ] →
          {S : σ → C} →
            [inst_3 : CategoryTheory.Limits.HasBiproduct S] →
              {T : τ → C} →
                [inst_4 : CategoryTheory.Limits.HasBiproduct T] →
                  (s : σ) →
                    CategoryTheory.CategoryStruct.id (S s) ≠ 0 →
                      (f : ⨁ S ⟶ ⨁ T) →
                        [CategoryTheory.IsIso f] →
                          Trunc
                            ((t : τ) ×'
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι S s)
                                  (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π T t)) ≠
                                0)
-- Mathlib.ModelTheory.PartialEquiv
/-- An alternate characterization of an extension pair is that every finitely generated partial
isomorphism can be extended to include any particular element of the domain.  -/
FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M),
      S.FG → ∀ (f : L.Embedding (↥S) N) (m : M), ∃ g, f = g.comp (FirstOrder.Language.Substructure.inclusion ⋯)
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_smul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → ∀ (f : F), derivWithin (fun y => c y • f) s x = derivWithin c s x • f
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coeAlgHom_of : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring S]
  [inst_3 : Semiring R] [inst_4 : Algebra S R] (A : ι → Submodule S R) [inst_5 : SetLike.GradedMonoid A] (i : ι)
  (x : ↥(A i)), (DirectSum.coeAlgHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
-- Mathlib.Data.Finsupp.Order
Finsupp.instSMulPosStrictMono : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : Zero β]
  [inst_3 : PartialOrder β] [inst_4 : SMulWithZero α β] [SMulPosStrictMono α β], SMulPosStrictMono α (ι →₀ β)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_eq_zero : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁺ = 0 ↔ a ≤ 0
-- Std.Time.Format.Modifier
Std.Time.Modifier.q.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.q presentation = Std.Time.Modifier.q presentation_1) = (presentation = presentation_1)
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C)
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType X₁ × CategoryTheory.ToType X₂),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)
      ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂).symm x) =
    x.2
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Option.isSome.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some val => h_1 val
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.Order.Heyting.Hom
map_hnot : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CoheytingAlgebra α]
  [inst_2 : CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α), f (￢a) = ￢f a
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_trace : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Module.Free R S]
  [Module.Finite R S] [Module.Free S T] [Module.Finite S T] (x : T),
  (Algebra.trace R S) ((Algebra.trace S T) x) = (Algebra.trace R T) x
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
/-- A `ℚ`-basis of `K` that spans `I` over `ℤ`, see `mem_span_basisOfFractionalIdeal` below.  -/
NumberField.basisOfFractionalIdeal : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) →
        Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℚ K
-- Mathlib.Algebra.Order.Group.MinMax
max_zero_sub_max_neg_zero_eq_self : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), max a 0 - max (-a) 0 = a
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.toAddMonoidHom : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → {S : AddGroupExtension N E G} → S.Splitting → G →+ E
-- Mathlib.Algebra.BigOperators.Pi
FunLike.coe_prod : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : CommMonoid β]
  [inst_2 : CommMonoid F] [IsOneApply F α β] [IsMulApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)