mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.SimpleFunc.integral_eq_sum : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [CompleteSpace E] (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) μ → ∫ (x : α), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x
-- Mathlib.Order.BooleanGenerators
/-- **Alias** of `IsCompactlyGenerated.BooleanGenerators.distribLatticeOfSSupEqTop`.

---

A lattice generated by Boolean generators is a distributive lattice.  -/
IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top : {α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} → [IsCompactlyGenerated α] → IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → DistribLattice α
-- Init.Tactics
/-- `with_reducible tacs` executes `tacs` using the reducible transparency setting.
In this setting only definitions tagged as `[reducible]` are unfolded.
 -/
Lean.Parser.Tactic.withReducible : Lean.ParserDescr
-- Mathlib.Control.Functor
Functor.Comp.instSeq : {F : Type u → Type w} → {G : Type v → Type u} → [Applicative F] → [Applicative G] → Seq (Functor.Comp F G)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k k' : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).getKey? k' =
        if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.id_comp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  (FirstOrder.Language.Hom.id L N).comp f = f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ),
  curr + 1 ≤ w →
    ∀ (acc lhs rhs : aig.RefVec w) (lexpr rexpr : BitVec w) (assign : α → Bool),
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx) →
          (∀ (idx : ℕ) (hidx : idx < w),
              ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx) →
            ∀ (idx : ℕ) (hidx : idx < w),
              ⟦assign,
                  { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs (curr + 1) acc).aig,
                    ref :=
                      (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs (curr + 1) acc).vec.get idx hidx }⟧ =
                (lexpr.mulRec rexpr w).getLsbD idx
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm_apply : ∀ (z : UpperHalfPlane), ModularForm.E₄CubeSubE₆SqForm✝ z = ModularForm.E₄ z ^ 3 - ModularForm.E₆ z ^ 2
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpolyRev.congr_simp : ∀ {R : Type u} [inst : CommRing R] {n : Type v} {inst_1 : DecidableEq n} [inst_2 : DecidableEq n] [inst_3 : Fintype n]
  (M M_1 : Matrix n n R), M = M_1 → M.charpolyRev = M_1.charpolyRev
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousSemilinearEquivClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  {M : outParam (Type u_4)} [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] {M₂ : outParam (Type u_5)}
  [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M] [inst_9 : Module S M₂]
  [inst_10 : EquivLike F M M₂] [toSemilinearEquivClass : SemilinearEquivClass F σ M M₂],
  autoParam (∀ (f : F), Continuous ⇑f) ContinuousSemilinearEquivClass.map_continuous._autoParam →
    autoParam (∀ (f : F), Continuous (EquivLike.inv f)) ContinuousSemilinearEquivClass.inv_continuous._autoParam →
      ContinuousSemilinearEquivClass F σ M M₂
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_add_eq_iff_eq_add : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b c : α}, ↑(-a) + b = c ↔ b = ↑a + c
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.brecOn : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} {a : Set α}
  (t : TopologicalSpace.GenerateOpen g a),
  (∀ (a : Set α) (t : TopologicalSpace.GenerateOpen g a), TopologicalSpace.GenerateOpen.below t → motive a t) →
    motive a t
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {x : M},
  s ⊆ f.source → x ∈ f.source → ↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhds (↑(f.extend I) x)] ↑(f.extend I) '' s
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.empty_mem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetSemiring C → ∅ ∈ C
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) (t : Set β),
  e.IsImage s t = ∀ ⦃x : α⦄, x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A morphism that only maps the zero pseudoelement to zero is a monomorphism.  -/
CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0) →
    CategoryTheory.Mono f
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.coe_mabs : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β] [inst_4 : Lattice β] [inst_5 : TopologicalLattice β] (f : C(α, β)), ⇑|f|ₘ = |⇑f|ₘ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
/-- This invariant states that if the `assignments` field of a default formula `f` indicates that `f`
contains an assignment `b` at index `i`, then the unit literal `(i, b)` is entailed by `f`. This is
distinct from the `StrongAssignmentsInvariant` defined above in that the entailment described here
does not require explicitly containing the literal `(i, b)`. For example, if `f` contains `(i, b) ∨ (j, b')`
as well as `(i, b) ∨ (j, ¬b')`, then the `AssignmentsInvariant` would permit the `assignments` field of `f`
to contain assignment `b` at index `i`, but the `StrongAssignmentsInvariant` would not.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.AssignmentsInvariant : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Prop
-- Batteries.Data.RunningStats
/-- Number of data points,  -/
Batteries.RunningStats.count : Batteries.RunningStats → ℕ
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquiv_symm_mk : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (I : Ideal R) (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : S),
  (I.quotientEquiv J f hIJ).symm ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f.symm x)
-- Init.Tactics
/-- `rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.
If `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.
If `e` is a defined constant, then the equational theorems associated with `e` are used.
This provides a convenient way to unfold `e`.
- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.
- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a
  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
  can also be used, to signify the target of the goal.

Using `rw (occs := .pos L) [e]`,
where `L : List Nat`, you can control which "occurrences" are rewritten.
(This option applies to each rule, so usually this will only be used with a single rule.)
Occurrences count from `1`.
At each allowed occurrence, arguments of the rewrite rule `e` may be instantiated,
restricting which later rewrites can be found.
(Disallowed occurrences do not result in instantiation.)
`(occs := .neg L)` allows skipping specified occurrences.
 -/
Lean.Parser.Tactic.rewriteSeq : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- For probability `p ≠ 0.5`, `binEntropy p < log 2`.  -/
Real.binEntropy_lt_log_two : ∀ {p : ℝ}, Real.binEntropy p < Real.log 2 ↔ p ≠ 2⁻¹
-- Mathlib.Data.Finmap
Finmap.mem_replace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b : β a} {s : Finmap β},
  a' ∈ Finmap.replace a b s ↔ a' ∈ s
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A multiplicative equivalence of groups preserves inversion.  -/
MulEquiv.map_inv : ∀ {G : Type u_7} {H : Type u_8} [inst : Group G] [inst_1 : DivisionMonoid H] (h : G ≃* H) (x : G), h x⁻¹ = (h x)⁻¹
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_map_of_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → f x ∈ Submonoid.map f S
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.rightAdjointObjIsDefined_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (Y : D), F.rightAdjointObjIsDefined Y
-- Init.Data.BitVec.Bitblast
Bool.atLeastTwo_true_left : ∀ {b c : Bool}, true.atLeastTwo b c = (b || c)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {n : ℕ}, n ≠ 0 → n • ∅ = ∅
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B} {a : A},
  (MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a = 0 ↔ f a = 0
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Iter.Equiv.trans : ∀ {α₁ α₂ α₃ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [inst_2 : Std.Iterator α₃ Id β]
  {ita : Std.Iter β} {itb : Std.Iter β} {itc : Std.Iter β}, ita.Equiv itb → itb.Equiv itc → ita.Equiv itc
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.mk.inj : ∀ {defaultInstances : Lean.NameMap (List (Lean.Name × ℕ))} {priorities : Lean.Meta.PrioritySet}
  {defaultInstances_1 : Lean.NameMap (List (Lean.Name × ℕ))} {priorities_1 : Lean.Meta.PrioritySet},
  { defaultInstances := defaultInstances, priorities := priorities } =
      { defaultInstances := defaultInstances_1, priorities := priorities_1 } →
    defaultInstances = defaultInstances_1 ∧ priorities = priorities_1
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄}
  (f f_1 :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A)),
  f = f_1 →
    CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f =
      CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst : ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f: M → N` and `g: M' → N'` are submersions at `x` and `x'`, respectively,
then `f × g: M × M' → N × N'` is a submersion at `(x, x')`.  -/
Manifold.IsSubmersionAtOfComplement.prodMap : ∀ {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {F : Type u_5} {F' : Type u_6} {H : Type u_7}
  {H' : Type u_8} {G : Type u_9} {G' : Type u_10} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E']
  [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E'']
  [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E'''] [inst_9 : NormedAddCommGroup F]
  [inst_10 : NormedSpace 𝕜 F] [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F']
  [inst_13 : TopologicalSpace H] [inst_14 : TopologicalSpace H'] [inst_15 : TopologicalSpace G]
  [inst_16 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} {M' : Type u_12} {N : Type u_13}
  {N' : Type u_14} [inst_17 : TopologicalSpace M] [inst_18 : ChartedSpace H M] [inst_19 : TopologicalSpace M']
  [inst_20 : ChartedSpace H' M'] [inst_21 : TopologicalSpace N] [inst_22 : ChartedSpace G N]
  [inst_23 : TopologicalSpace N'] [inst_24 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {g : M' → N'}
  {x' : M'} [IsManifold I n M] [⋯], ⋯
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.comp_apply : ∀ {M N T : AddMagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.mk_eq : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {f g : PadicSeq p}, Padic.mk f = Padic.mk g ↔ f ≈ g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.toIdeal_comap : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ},
  (HomogeneousIdeal.comap f J).toIdeal = Ideal.comap f J.toIdeal
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_of_nonneg' : ∀ {K : Type u_1} [inst : RCLike K] {x : K}, 0 ≤ x → ↑‖x‖ = x
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).hom.app P).f.f = P.p.f
-- Init.Data.UInt.Lemmas
UInt8.add_left_neg : ∀ (a : UInt8), -a + a = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instAddErrorMessageContextTermElabM : Lean.AddErrorMessageContext Lean.Elab.TermElabM
-- Mathlib.Topology.Connected.TotallyDisconnected
Prod.totallyDisconnectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [TotallyDisconnectedSpace α]
  [TotallyDisconnectedSpace β], TotallyDisconnectedSpace (α × β)
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- Analogue of `ord_ne_top` for `ordMonoidWithZeroHom`.
 -/
Ring.ordMonoidWithZeroHom_ne_zero : ∀ {R : Type u_2} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] [inst_3 : Nontrivial R] {a : R},
  a ∈ nonZeroDivisors R → (Ring.ordMonoidWithZeroHom R) a ≠ 0
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.renameProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.RenameOptions
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.postcomp_uniq : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation),
  solution.postcomp ↑(h.uniq h') = solution'
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearMap_apply : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] N) (g : α →₀ M), (Finsupp.mapRange.linearMap f) g = Finsupp.mapRange ⇑f ⋯ g
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.commShiftι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.ObjectProperty C) →
      {A : Type u_2} →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] → [inst_3 : P.IsStableUnderShift A] → P.ι.CommShift A
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_eq_const : ∀ {α : Type u_1} {K : Type u_2} {t s : K} [inst : SMul K α], t = s → ∀ (c : α), t • c = s • c
-- Mathlib.Data.Nat.Size
Nat.size_bit : ∀ {b : Bool} {n : ℕ}, Nat.bit b n ≠ 0 → (Nat.bit b n).size = n.size.succ
-- Mathlib.Order.WithBot
WithTop.strictAnti_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithTop α → β},
  StrictAnti f ↔ (StrictAnti fun a => f ↑a) ∧ ∀ (x : α), f ⊤ < f ↑x
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
/-- When two morphisms `X ⟶ Y` with `Y` fibrant are related by a right homotopy,
this is a choice of a left homotopy relative to any good cylinder object for `X`.  -/
HomotopicalAlgebra.RightHomotopyRel.leftHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [HomotopicalAlgebra.IsFibrant Y] →
            HomotopicalAlgebra.RightHomotopyRel f g →
              (Q : HomotopicalAlgebra.Cylinder X) → [Q.IsGood] → Q.LeftHomotopy f g
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.finSuccEquiv_X_succ : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (j : Fin n),
  (MvPowerSeries.finSuccEquiv R n) (MvPowerSeries.X j.succ) = PowerSeries.C (MvPowerSeries.X j)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates coequalizers and finite coproducts, it creates finite colimits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating colimits" in the literature, and whether or not the condition can be dropped seems to
depend on the specific definition that is used.  -/
CategoryTheory.Limits.createsFiniteColimitsOfCreatesCoequalizersAndFiniteCoproducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasCoequalizers D] →
          [CategoryTheory.Limits.HasFiniteCoproducts D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                  [CategoryTheory.Limits.CreatesFiniteCoproducts G] → CategoryTheory.Limits.CreatesFiniteColimits G
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_map_of_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Bijective ⇑f → ∀ {I : Ideal R}, Ideal.comap f (Ideal.map f I) = I
-- Mathlib.Data.PEquiv
PEquiv.single_apply_of_ne : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] {a₁ a₂ : α},
  a₁ ≠ a₂ → ∀ (b : β), (PEquiv.single a₁ b) a₂ = none
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_ball_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {p : α → (i : ι) → i ∈ S → Prop},
      (∀ᵐ (x : α) ∂μ, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᵐ (x : α) ∂μ, p x i hi
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addMeasure_map_restrict_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (s : Set α) {U : Set (Quotient (AddAction.orbitRel G α))},
  MeasurableSet U →
    (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s)) U =
      μ (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ s)
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Extends the domain of a `HahnSeries` by an `OrderEmbedding`.  -/
HahnSeries.embDomain : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] → [inst_2 : PartialOrder Γ'] → Γ ↪o Γ' → HahnSeries Γ R → HahnSeries Γ' R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey? k' =
    if compare k k' = Ordering.eq then
      if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then some k else none
    else t.getKey? k'
-- Mathlib.Data.Sum.Order
OrderIso.emptySumLex_apply_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] [inst_2 : IsEmpty β] (x : α),
  OrderIso.emptySumLex (toLex (Sum.inr x)) = x
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCancelCommMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCancelCommMonoid (f i)] → AddCancelCommMonoid ((i : I) → f i)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.erase_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}, ∅.erase a = ∅
-- Std.Time.Duration
Std.Time.instReprDuration : Repr Std.Time.Duration
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul_of_tower_mem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {x : M} [inst_2 : SMul S R] [inst_3 : SMul S M] [IsScalarTower S R M] (r : S), x ∈ p → r • x ∈ p
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rcc_eq_fallback : ∀ {m n i fallback : ℕ}, n + 1 ≤ i + m → (m...=n).toArray.getD i fallback = fallback