mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_derivedLits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (rupHints : Array ℕ) (f'_assignments_size : (f.performRupCheck rupHints).1.assignments.size = n)
  (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).1.assignments f'_assignments_size derivedLits →
    ∀ (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
      derivedLits_arr = { toList := derivedLits } →
        ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
-- Mathlib.Analysis.Seminorm
Seminorm.coe_restrictScalars : ∀ (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜']
  [inst_2 : SMul 𝕜 𝕜'] [inst_3 : NormSMulClass 𝕜 𝕜'] [inst_4 : NormOneClass 𝕜'] [inst_5 : AddCommGroup E]
  [inst_6 : Module 𝕜' E] [inst_7 : SMul 𝕜 E] [inst_8 : IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E),
  ⇑(Seminorm.restrictScalars 𝕜 p) = ⇑p
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Make an isomorphism between triangles from the required data.  -/
CategoryTheory.Pretriangulated.Triangle.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (A B : CategoryTheory.Pretriangulated.Triangle C) →
        (iso₁ : A.obj₁ ≅ B.obj₁) →
          (iso₂ : A.obj₂ ≅ B.obj₂) →
            (iso₃ : A.obj₃ ≅ B.obj₃) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom =
                    CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁)
                  CategoryTheory.Pretriangulated.Triangle.isoMk._auto_1 →
                autoParam
                    (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom =
                      CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂)
                    CategoryTheory.Pretriangulated.Triangle.isoMk._auto_3 →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) =
                        CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃)
                      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_5 →
                    (A ≅ B)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_fstX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (HomologicalComplex.homotopyCofiber.fstX φ i j hij) =
    0
-- Mathlib.Analysis.Normed.Ring.Basic
NormOneClass.mk : ∀ {α : Type u_5} [inst : Norm α] [inst_1 : One α], ‖1‖ = 1 → NormOneClass α
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.MonoidAlgebra.mapDomainOfBialgHomFun.eq_1 : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G),
  MonoidAlgebra.mapDomainOfBialgHomFun✝ f g = Exists.choose ⋯
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGEFunctor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  {X Y : HomologicalComplex C c'} (φ : X ⟶ Y), (e.truncGEFunctor C).map φ = HomologicalComplex.truncGEMap φ e
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4)
  (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.halt with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_6 ()
-- Mathlib.Data.List.Sigma
List.kerase_comm : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a₁ a₂ : α) (l : List (Sigma β)),
  List.kerase a₂ (List.kerase a₁ l) = List.kerase a₁ (List.kerase a₂ l)
-- Mathlib.Order.CompleteSublattice
/-- We can regard a complete lattice homomorphism as an order equivalence to its range.  -/
CompleteLatticeHom.toOrderIsoRangeOfInjective : {α : Type u_1} →
  {β : Type u_2} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] → (f : CompleteLatticeHom α β) → Function.Injective ⇑f → α ≃o ↥f.range
-- Mathlib.Data.PNat.Basic
PNat.instIsBotOneClass : IsBotOneClass ℕ+
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.mk.injEq : ∀ (processId? : Option ℤ) (clientInfo? : Option Lean.Lsp.ClientInfo) (rootUri? : Option String)
  (initializationOptions? : Option Lean.Lsp.InitializationOptions) (capabilities : Lean.Lsp.ClientCapabilities)
  (trace : Lean.Lsp.Trace) (workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)) (processId?_1 : Option ℤ)
  (clientInfo?_1 : Option Lean.Lsp.ClientInfo) (rootUri?_1 : Option String)
  (initializationOptions?_1 : Option Lean.Lsp.InitializationOptions) (capabilities_1 : Lean.Lsp.ClientCapabilities)
  (trace_1 : Lean.Lsp.Trace) (workspaceFolders?_1 : Option (Array Lean.Lsp.WorkspaceFolder)),
  ({ processId? := processId?, clientInfo? := clientInfo?, rootUri? := rootUri?,
        initializationOptions? := initializationOptions?, capabilities := capabilities, trace := trace,
        workspaceFolders? := workspaceFolders? } =
      { processId? := processId?_1, clientInfo? := clientInfo?_1, rootUri? := rootUri?_1,
        initializationOptions? := initializationOptions?_1, capabilities := capabilities_1, trace := trace_1,
        workspaceFolders? := workspaceFolders?_1 }) =
    (processId? = processId?_1 ∧
      clientInfo? = clientInfo?_1 ∧
        rootUri? = rootUri?_1 ∧
          initializationOptions? = initializationOptions?_1 ∧
            capabilities = capabilities_1 ∧ trace = trace_1 ∧ workspaceFolders? = workspaceFolders?_1)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.LocalTimeType.mk.inj : ∀ {gmtOffset : Std.Time.TimeZone.Offset} {isDst : Bool} {abbreviation : String} {wall : Std.Time.TimeZone.StdWall}
  {utLocal : Std.Time.TimeZone.UTLocal} {identifier : String} {gmtOffset_1 : Std.Time.TimeZone.Offset} {isDst_1 : Bool}
  {abbreviation_1 : String} {wall_1 : Std.Time.TimeZone.StdWall} {utLocal_1 : Std.Time.TimeZone.UTLocal}
  {identifier_1 : String},
  { gmtOffset := gmtOffset, isDst := isDst, abbreviation := abbreviation, wall := wall, utLocal := utLocal,
        identifier := identifier } =
      { gmtOffset := gmtOffset_1, isDst := isDst_1, abbreviation := abbreviation_1, wall := wall_1,
        utLocal := utLocal_1, identifier := identifier_1 } →
    gmtOffset = gmtOffset_1 ∧
      isDst = isDst_1 ∧ abbreviation = abbreviation_1 ∧ wall = wall_1 ∧ utLocal = utLocal_1 ∧ identifier = identifier_1
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_sdiff_botSet : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) {s : Set R},
  f.length (s \ botSet) = f.length s
-- Mathlib.Data.Seq.Computation
Computation.map_think' : ∀ {α β : Type u_1} (f : α → β) (s : Computation α), f <$> s.think = (f <$> s).think
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_lt_lowerCrossingTime : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.lowerCrossingTime a b f N (n + 1) ω ≠ N →
      MeasureTheory.upperCrossingTime a b f N (n + 1) ω < MeasureTheory.lowerCrossingTime a b f N (n + 1) ω
-- Mathlib.Algebra.Quaternion
Quaternion.star_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a.im = -a.im
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.forbidden.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] [inst_1 : AddMonoid G]
  (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  SymbolicDynamics.FullShift.forbidden F = {x | ∀ p ∈ F, ∀ (g : G), ¬p.occursInAt x g}
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Real.tendsto_mul_log_one_add_div_atTop : ∀ (t : ℝ), Filter.Tendsto (fun x => x * Real.log (1 + t / x)) Filter.atTop (nhds t)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- [Stacks Tag 0FX2](https://stacks.math.columbia.edu/tag/0FX2) (second part) -/
CategoryTheory.ObjectProperty.retractClosure_extensionProduct_retractClosure_retractClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C),
  (P.retractClosure.extensionProduct Q.retractClosure).retractClosure = (P.extensionProduct Q).retractClosure
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.bisim : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop),
  (∀ (x y : P.M α),
      R x y →
        ∃ a f f₁ f₂,
          MvPFunctor.M.dest P x = ⟨a, TypeVec.splitFun f f₁⟩ ∧
            MvPFunctor.M.dest P y = ⟨a, TypeVec.splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)) →
    ∀ (x y : P.M α), R x y → x = y
-- Mathlib.Computability.Partrec
Nat.mem_rfind : ∀ {p : ℕ →. Bool} {n : ℕ}, n ∈ Nat.rfind p ↔ true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_intro : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop) (h : l),
  Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp p) h =
    (p → Lean.Order.PartialOrder.rel Lean.Order.top h)
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.mk.inj : ∀ {toCacheableParserContext : Lean.Parser.CacheableParserContext} {parserName : Lean.Name} {pos : String.Pos.Raw}
  {toCacheableParserContext_1 : Lean.Parser.CacheableParserContext} {parserName_1 : Lean.Name} {pos_1 : String.Pos.Raw},
  { toCacheableParserContext := toCacheableParserContext, parserName := parserName, pos := pos } =
      { toCacheableParserContext := toCacheableParserContext_1, parserName := parserName_1, pos := pos_1 } →
    toCacheableParserContext = toCacheableParserContext_1 ∧ parserName = parserName_1 ∧ pos = pos_1
-- Mathlib.NumberTheory.Padics.WithVal
Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], ↑Padic.withValUniformEquiv = ↑Padic.withValRingEquiv
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- The parameterized integral `x ↦ ∫ y, g (-y + x) ∂μ` depends continuously on `y`
when `g` is a compactly supported continuous function on a topological additive group `G`, and `μ`
is finite on compact sets.  -/
MeasureTheory.continuous_integral_apply_neg_add : ∀ {G : Type u_1} [inst : TopologicalSpace G] [LocallyCompactSpace G] [inst_2 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : NormedSpace ℝ E] {g : G → E},
  Continuous g → HasCompactSupport g → Continuous fun x => ∫ (y : G), g (-y + x) ∂μ
-- Init.Omega.Int
Lean.Omega.Prod.of_lex : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {p q : α × β},
  Prod.Lex r s p q → r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2
-- Init.Data.List.Basic
List.drop_zero : ∀ {α : Type u} {l : List α}, List.drop 0 l = l
-- Mathlib.Order.SymmDiff
bihimp_inf_sup : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b ⊓ (a ⊔ b) = a ⊓ b
-- Mathlib.Algebra.Tropical.Basic
Tropical.decidableLE : {R : Type u} → [inst : LE R] → [DecidableLE R] → DecidableLE (Tropical R)
-- Mathlib.Data.EReal.Operations
EReal.add_bot : ∀ (x : EReal), x + ⊥ = ⊥
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_obj_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L')),
  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).left = X.left
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous on a set `S`, the same is true for its closure in *any*
topology for which evaluation at any `x ∈ S` is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.EquicontinuousOn.closure` for a more familiar
(but weaker) statement.  -/
EquicontinuousOn.closure' : ∀ {X : Type u_3} {Y : Type u_5} {α : Type u_6} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [uα : UniformSpace α]
  {A : Set Y} {u : Y → X → α} {S : Set X},
  EquicontinuousOn (u ∘ Subtype.val) S → Continuous (S.domRestrict ∘ u) → EquicontinuousOn (u ∘ Subtype.val) S
-- Mathlib.Topology.Algebra.Semigroup
/-- Any nonempty compact Hausdorff semigroup where right-multiplication is continuous contains
an idempotent, i.e. an `m` such that `m * m = m`.  -/
exists_idempotent_of_compact_t2_of_continuous_mul_left : ∀ {M : Type u_1} [Nonempty M] [inst : Semigroup M] [inst_1 : TopologicalSpace M] [CompactSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x * r) → ∃ m, m * m = m
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_2 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (isLt_1 : 1 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨1, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_2 isLt isLt_1 x
-- Mathlib.Algebra.WithConv
WithConv.ofConv_add : ∀ {A : Type u_2} [inst : AddMonoid A] (x y : WithConv A), (x + y).ofConv = x.ofConv + y.ofConv
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.self_trans_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β), e.trans e.symm = OrderRingIso.refl α
-- Mathlib.Logic.Function.ULift
PLift.down_inj : ∀ {α : Sort u_1} {a b : PLift α}, a.down = b.down ↔ a = b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toList.toArray = t.toArray
-- Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
/-- The integral of `log ∘ sin` on `0 … π/2` equals `-log 2 * π / 2`.
 -/
integral_log_sin_zero_pi_div_two : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) = -Real.log 2 * Real.pi / 2
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.cast_symm_apply : ∀ {R : Type uR} [inst : CommSemiring R] {ι : Type u_1} {A : ι → Type u_2} [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {i j : ι} (h : i = j) (a : A j), (AlgEquiv.cast h).symm a = cast ⋯ a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ε_def : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.Functor.LaxMonoidal.ε (Rep.linearization k G) = Rep.ofHom (Representation.LinearizeMonoidal.ε k G)
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_iff_not_tendsto_nat_atTop_of_nonneg : ∀ {f : ℕ → ℝ},
  (∀ (n : ℕ), 0 ≤ f n) → (Summable f ↔ ¬Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.isometry_lpMeasSubgroupToLpTrim : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hp : Fact (1 ≤ p)] (hm : m ≤ m0),
  Isometry (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L : CategoryTheory.Functor C D) (X : C) (f : K ⟶ K)
  (x :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type (max (max u v) v'))) ((K.functorHom L).obj X)),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.Functor.natTransEquiv.symm f).app X)
          ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))))
      x =
    (CategoryTheory.Functor.HomObj.ofNatTrans f, x.2)
-- Mathlib.Algebra.MvPolynomial.Division
/-- Divide by `monomial 1 s`, discarding terms not divisible by this.  -/
MvPolynomial.divMonomial : {σ : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → (σ →₀ ℕ) → MvPolynomial σ R
-- Mathlib.Topology.Order.Lattice
TopologicalLattice.mk : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Lattice L] [toContinuousInf : ContinuousInf L]
  [toContinuousSup : ContinuousSup L], TopologicalLattice L
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- Given a simplex `x : X.S` of a simplicial set `X`, this is the unique
(epi)morphism `f : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌` such that `x.simplex` is
`X.map f.op x.toN.simplex` where `x.toN : X.N` is the unique nondegenerate
simplex of `X` which generates the same subcomplex as `x`.  -/
SSet.S.toNπ : {X : SSet} → (x : X.S) → { len := x.dim } ⟶ { len := x.toN.dim }
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
StarRingEquiv.mk.congr_simp : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (toRingEquiv toRingEquiv_1 : A ≃+* B) (e_toRingEquiv : toRingEquiv = toRingEquiv_1)
  (map_star' : ∀ (a : A), toRingEquiv.toFun (star a) = star (toRingEquiv.toFun a)),
  { toRingEquiv := toRingEquiv, map_star' := map_star' } = { toRingEquiv := toRingEquiv_1, map_star' := ⋯ }
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodCongr_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] {module_M : Module R M}
  {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄)
  (p : M × M₃), (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mk'.congr_simp : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (carrier carrier_1 : Set R) (e_carrier : carrier = carrier_1)
  (zero_mem : 0 ∈ carrier) (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
  (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier) (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
  (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier),
  TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right = TwoSidedIdeal.mk' carrier_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_im_nonneg_of_ne_zero : ∀ {z : ℂ}, 0 ≤ z.im → z ≠ 0 → z.arg = Real.arccos (z.re / ‖z‖)
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.subst : Lean.Meta.CaseValuesSubgoal → Lean.Meta.FVarSubst
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.addPart : Lean.VersoModuleDocs.Snippet →
  ℕ → Lean.DeclarationRange → Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty → Lean.VersoModuleDocs.Snippet
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_toMeasurable : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ ⊤ → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F),
  CategoryTheory.Functor.CoconeTypes.IsColimit c.cofanTypes ↔ Nonempty (CategoryTheory.Limits.IsColimit c)
-- Mathlib.Data.Set.Image
Set.subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, t ⊆ f '' s ↔ ∃ u ⊆ s, f '' u = t
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.mem_neg : ∀ {G : Type u_2} [inst : AddGroup G] {g : G} {S : AddSubmonoid G}, g ∈ -S ↔ -g ∈ S
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_monomial_mapDomain : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : σ →₀ ℕ} {c : R},
  (MvPolynomial.killCompl hf) ((MvPolynomial.monomial (Finsupp.mapDomain f s)) c) = (MvPolynomial.monomial s) c
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.isHomogeneous : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  (R : HomogeneousSubsemiring 𝒜), DirectSum.SetLike.IsHomogeneous 𝒜 R
-- Mathlib.RepresentationTheory.Invariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` restricts to a `G`-representation on
the invariants of `ρ|_S`.  -/
Rep.toInvariants : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] → [inst_1 : Group G] → Rep.{w, u, v} k G → (S : Subgroup G) → [S.Normal] → Rep.{w, u, v} k G
-- Lean.Util.CollectFVars
Lean.CollectFVars.Visitor : Type
-- Init.Data.Ord.Basic
Ordering.eq.sizeOf_spec : sizeOf Ordering.eq = 1