mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Operations
Submodule.smul_eq_map₂ : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Ideal R}
  {N : Submodule R M}, I • N = Submodule.map₂ (LinearMap.lsmul R M) I N
-- Mathlib.Data.PEquiv
PEquiv.isSome_symm_get : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : (f a).isSome = true), (f.symm ((f a).get h)).isSome = true
-- Mathlib.Data.Nat.Cast.Commute
Nat.addCommute_cast_one : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ℕ), AddCommute (↑n) 1
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv]
  (f g : CauSeq β abv), f.lim - g.lim = (f - g).lim
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} (a : α),
  MeasurableSet s → (MeasureTheory.Measure.dirac a) s = s.indicator 1 a
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.neg : ∀ {Ω : 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} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Submartingale (-f) ℱ μ
-- Std.Data.Iterators.Combinators.Monadic.Zip
Option.SomeLtNone.lt.eq_2 : ∀ {β : Type u_1} {α : Type u_2} (r : α → β → Prop) (val : α), Option.SomeLtNone.lt r (some val) none = True
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (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.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves finite products, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
coproducts.  -/
CategoryTheory.Limits.preservesFiniteCoproducts_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F.op
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.cast_eq_cast : ∀ {n m : ℕ} (c : Composition m) (hmn : m = n), c.cast hmn = cast ⋯ c
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.map_map : ∀ {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter α) (m : α → β) (n : β → γ),
  Ultrafilter.map n (Ultrafilter.map m f) = Ultrafilter.map (n ∘ m) f
-- Mathlib.Topology.Sheaves.Skyscraper
SkyscraperPresheafFunctor.map'_comp : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {a b c : C} (f : a ⟶ b)
  (g : b ⟶ c),
  SkyscraperPresheafFunctor.map' p₀ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (SkyscraperPresheafFunctor.map' p₀ f) (SkyscraperPresheafFunctor.map' p₀ g)
-- Mathlib.Data.Real.ENatENNReal
/-- Coercion `ℕ∞ → ℝ≥0∞` as a ring homomorphism.  -/
ENat.toENNRealRingHom : ℕ∞ →+* ENNReal
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `G` is `H`-free, then `G` has at most `extremalNumber (card V) H` edges.  -/
SimpleGraph.card_edgeFinset_le_extremalNumber : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj], H.Free G → G.edgeFinset.card ≤ SimpleGraph.extremalNumber (Fintype.card V) H
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Elaborate a `#rw??` command.  -/
Mathlib.Tactic.LibraryRewrite.elabrw??Command : Lean.Elab.Command.CommandElab
-- Lean.Elab.Match
/-- Applies `whnf` but tries to preserve `PatternWithRef` information.
This is a bit hackish, but it is necessary for providing proper
jump-to-definition information in examples such as
```
def f (x : Nat) : Nat :=
  match x with
  | 0 => 1
  | y + 1 => y
```
Without this trick, the `PatternWithRef` is lost for the `y` at the pattern `y+1`.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.whnfPreservingPatternRef : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_bot'`. -/
Ideal.ramificationIdx_bot' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R},
  p ≠ ⊥ → Function.Injective ⇑(algebraMap R S) → p.ramificationIdx' ⊥ = 0
-- Lean.Elab.Command
/-- The expanded syntax tree.  -/
Lean.Elab.Command.MacroExpandedSnapshot.newStx : Lean.Elab.Command.MacroExpandedSnapshot → Lean.Syntax
-- Mathlib.Order.OmegaCompletePartialOrder
Part.ωSup_eq_some : ∀ {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α}, Part.some a ∈ c → Part.ωSup c = Part.some a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_obj₁_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (X : C) (n : ℤ),
  t.IsLE (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X).obj₁ (n - 1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addMonoid : {α : Type u} → [AddMonoid α] → AddMonoid (WithTop α)
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
IsValuativeTopology.v_eq_valuation : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : UniformSpace R] [inst_3 : IsUniformAddGroup R]
  [inst_4 : IsValuativeTopology R], Valued.v = ValuativeRel.valuation R
-- Mathlib.Topology.Order.Bornology
BddBelow.isBounded : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddBelow s → BddAbove s → Bornology.IsBounded s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey? = t.minKey? ↔
    ∀ {km : α}, t.minKey? = some km → ¬compare k km = Ordering.eq
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.inf_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeInf β]
  [inst_3 : ContinuousInf β] (f g : C(α, β)) (a : α), (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.one_sub_iff : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem (1 - a) ↔ IsIdempotentElem a
-- Mathlib.Algebra.Group.TransferInstance
Equiv.vadd_def : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : VAdd M β] (n : M) (x : α), n +ᵥ x = e.symm (n +ᵥ e x)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.instCompletableTopFieldWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), CompletableTopField (WithAbs ↑v)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).unitIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A morphism of additive monoid objects.  -/
CategoryTheory.AddMon.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.AddMon C → CategoryTheory.AddMon C → Type v₁
-- Mathlib.Data.Option.Basic
Option.map_inj : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β}, Option.map f = Option.map g ↔ f = g
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitForall : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Algebra.Category.GrpWithZero
Bipointed.Hom.mk.congr_simp : ∀ {X Y : Bipointed} (toFun toFun_1 : X.X → Y.X) (e_toFun : toFun = toFun_1) (map_fst : toFun X.toProd.1 = Y.toProd.1)
  (map_snd : toFun X.toProd.2 = Y.toProd.2),
  { toFun := toFun, map_fst := map_fst, map_snd := map_snd } = { toFun := toFun_1, map_fst := ⋯, map_snd := ⋯ }
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_trans : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n), ⇑(h₁.trans h₂) = ⇑h₂ ∘ ⇑h₁
-- Mathlib.Algebra.Group.Finsupp
Finsupp.update_eq_single_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {f : ι →₀ M} {a : ι},
  f a = 0 → ∀ (b : M), f.update a b = (fun₀ | a => b) + f
-- Init.Data.Iterators.Basic
Std.Iter.isPlausibleIndirectSuccessor_iff_isPlausibleIndirectSuccessor_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it' it : Std.Iter β},
  it'.IsPlausibleIndirectSuccessorOf it ↔ it'.toIterM.IsPlausibleIndirectSuccessorOf it.toIterM
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalAllGoals : Lean.Elab.Tactic.Tactic
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le : ∀ {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [Nonempty M] [inst : L.Structure M]
  [M ⊨ T],
  Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} (Cardinal.mk M) →
    ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_id : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) cfc_id._auto_1 → cfc id a = a
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.induce_comp_induce : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  {s : Set V} {t : Set W} {r : Set X} (φ : G ≃g G') (φst : Set.BijOn (⇑φ) s t) (ψ : G' ≃g G'')
  (ψtr : Set.BijOn (⇑ψ) t r), (ψ.induce ψtr).comp (φ.induce φst) = (ψ.comp φ).induce ⋯
-- Init.Data.Nat.Lemmas
Nat.sub_right_comm : ∀ (m n k : ℕ), m - n - k = m - k - n
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.basisQuotient.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : Module.Finite R S] [inst_5 : Module.Free R S] {ι : Type u_3} [inst_6 : Fintype ι]
  (b b_1 : Module.Basis ι R S), b = b_1 → IsLocalRing.basisQuotient b = IsLocalRing.basisQuotient b_1
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.ext_iff : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂},
  g = h ↔ (TensorProduct.mk R M N).compr₂ₛₗ g = (TensorProduct.mk R M N).compr₂ₛₗ h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v fallback : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l → Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.insertMany t l) k' fallback = v
-- Mathlib.Algebra.GroupWithZero.Prod
/-- Division as a multiplicative homomorphism with zero.  -/
divMonoidWithZeroHom : {M₀ : Type u_1} → [inst : CommGroupWithZero M₀] → M₀ × M₀ →*₀ M₀
-- Mathlib.RingTheory.Ideal.Basic
Ideal.add_pow_add_pred_mem_of_pow_mem : ∀ {α : Type u_2} {a b : α} [inst : CommSemiring α] (I : Ideal α) {m n : ℕ},
  a ^ m ∈ I → b ^ n ∈ I → (a + b) ^ (m + n - 1) ∈ I
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Characterisation of `2`-Freiman homs.  -/
isMulFreimanIso_two : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanIso 2 A B f ↔ Set.BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → s ∈ nhds x → DifferentiableAt 𝕜 f x
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_sub : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Sub α] (A B : Matrix m n α),
  (A - B).submatrix = A.submatrix - B.submatrix
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ColorFocused.mk : {α : Type u_5} →
  {ι : Type u_6} →
    {κ : Type u_7} →
      {C : (ι → Option α) → κ} →
        (lines : Multiset (Combinatorics.Line.AlmostMono C)) →
          (focus : ι → Option α) →
            (∀ p ∈ lines, ↑p.line none = focus) →
              (Multiset.map Combinatorics.Line.AlmostMono.color lines).Nodup → Combinatorics.Line.ColorFocused C
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.nnnorm_natCast_le_one : ∀ (R : Type u_1) [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (n : ℕ), ‖↑n‖₊ ≤ 1
-- Mathlib.Algebra.Ring.Equiv
/-- Gives a `RingEquiv` from an element of an `AddEquivClass` preserving addition.  -/
AddEquiv.toRingEquiv : {R : Type u_7} →
  {S : Type u_8} →
    {F : Type u_9} →
      [inst : Add R] →
        [inst_1 : Add S] →
          [inst_2 : Mul R] →
            [inst_3 : Mul S] →
              [inst_4 : EquivLike F R S] →
                [AddEquivClass F R S] → (f : F) → (∀ (x y : R), f (x * y) = f x * f y) → R ≃+* S
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolTag.deprecated.sizeOf_spec : sizeOf Lean.Lsp.SymbolTag.deprecated = 1
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.congr_simp : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] (b b_1 : ι → M),
  b = b_1 →
    ∀ {inst_4 : DecidableEq ι} [inst_5 : DecidableEq ι] (A A_1 : Matrix ι ι R),
      A = A_1 → ∀ (f f_1 : Module.End R M), f = f_1 → Matrix.Represents b A f = Matrix.Represents b_1 A_1 f_1
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.closedCounit_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X Y : (i : I) → C i) (i : I), (CategoryTheory.Pi.closedCounit X).app Y i = (CategoryTheory.ihom.ev (X i)).app (Y i)
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.eq_def : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }),
  ep.subtypeCongr en = (Equiv.sumCompl p).permCongr (ep.sumCongr en)
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a fallback : α},
  (m.insert k).getD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getD a fallback
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Theory.IsUniversal.models_of_embedding : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory} [hT : T.IsUniversal] {N : Type u_1}
  [inst_1 : L.Structure N] [N ⊨ T] (f : L.Embedding M N), M ⊨ T
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_ne_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ) [IsDomain R] [NeZero 2], n ≠ -1 → Polynomial.Chebyshev.U R n ≠ 0
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_mk_eq : ∀ {α : Type u} {β : Type v},
  Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace map is a left inverse of the algebra map.  -/
Algebra.normalizedTrace_algebraMap_eq_id : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K], Algebra.normalizedTrace F K ∘ₗ Algebra.linearMap F K = LinearMap.id
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.

`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findM?` always terminates after finitely many steps.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Std.Iter.findM? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → Std.Iter β → (β → m (ULift.{w, 0} Bool)) → m (Option β)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_stronglyMeasurable : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.StronglyMeasurable X →
    MeasureTheory.Integrable ((X - μ[X | m]) ^ 2) μ → ProbabilityTheory.condVar m X μ = fun ω => (X ω - μ[X | m] ω) ^ 2
-- Mathlib.Analysis.Calculus.Rademacher
/-- The line derivative of a Lipschitz function is almost everywhere linear with respect to fixed
coefficients.  -/
LipschitzWith.ae_lineDeriv_sum_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f →
    ∀ {ι : Type u_3} (s : Finset ι) (a : ι → ℝ) (v : ι → E),
      ∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.free.generatingSections_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u),
  (SheafOfModules.free.generatingSections I).π = CategoryTheory.CategoryStruct.id (SheafOfModules.free I)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_mul_eq_of_coprime_left : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R} [I.IsTwoSided], I ⊔ J = ⊤ → I ⊔ J * K = I ⊔ K
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The quotient by `MulAction.orbitRel`, given a name to enable dot notation.  -/
MulAction.orbitRel.Quotient : (G : Type u_1) → (α : Type u_2) → [inst : Group G] → [MulAction G α] → Type u_2
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Number of blocks in a `CompositionAsSet`.  -/
CompositionAsSet.length : {n : ℕ} → CompositionAsSet n → ℕ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), ↑E ⊆ C
-- Mathlib.Order.BoundedOrder.Monotone
Monotone.exists : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop},
  (∀ (x : β), Monotone (P x)) → Monotone fun y => ∃ x, P x y
-- Init.Data.Range.Polymorphic.SInt
Int32.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int32
-- Mathlib.Topology.Continuous
denseRange_subtype_val : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop}, DenseRange Subtype.val ↔ Dense {x | p x}
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift_comp_inrHom : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r),
  (TrivSqZeroExt.lift f g hg hfg hgf).toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) = g
-- Mathlib.Topology.EMetricSpace.Defs
/-- `WeakPseudoEMetricSpace` can be induced backwards.  -/
WeakPseudoEMetricSpace.IsInducing : {α : Type u_2} →
  {β : Type u_3} →
    [e : TopologicalSpace α] →
      [n : TopologicalSpace β] →
        {f : α → β} → Topology.IsInducing f → WeakPseudoEMetricSpace β → WeakPseudoEMetricSpace α
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The canonical comonoid structure on the monoidal unit.
This is not a global instance to avoid conflicts with other comonoid structures.  -/
CategoryTheory.ComonObj.instTensorUnit : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.ComonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.toFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) (x : C), S.toFunctor.obj x = MonCat.of ↥(S.obj x)
-- Mathlib.Data.Finset.Union
Finset.disjiUnion.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (s s_1 : Finset α) (e_s : s = s_1) (t t_1 : α → Finset β) (e_t : t = t_1)
  (hf : (↑s).PairwiseDisjoint t), s.disjiUnion t hf = s_1.disjiUnion t_1 ⋯