ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℚ → ℚ → ℚ<VAR>f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ<VAR>fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = Rat.divInt (f₁ n₁ (↑d₁) n₂ ↑d₂) (f₂ n₁ (↑d₁) n₂ ↑d₂)<VAR>f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<VAR>H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂<GOAL>f (Rat.divInt a b) (Rat.divInt c d) = Rat.divInt (f₁ a b c d) (f₂ a b c d)
<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<GOAL>Rat.divInt a b + Rat.divInt c d = Rat.divInt (a * d + c * b) (b * d)
<VAR>q : ℚ<GOAL>-q = Rat.divInt (-q.num) ↑q.den
<VAR>n d : ℤ<GOAL>Rat.divInt n (-d) = Rat.divInt (-n) d
<VAR>a b c d : ℤ<VAR>b0 : b ≠ 0<VAR>d0 : d ≠ 0<GOAL>Rat.divInt a b - Rat.divInt c d = Rat.divInt (a * d - c * b) (b * d)
<VAR>n₁ d₁ n₂ d₂ : ℤ<GOAL>Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)
<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>{ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
<VAR>q r : ℚ<GOAL>q * r = mkRat (q.num * r.num) (q.den * r.den)
<VAR>q : ℚ<VAR>n : ℕ<GOAL>q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ }
<VAR>q : ℚ<VAR>n : ℕ<GOAL>q ^ n = mkRat (q.num ^ n) (q.den ^ n)
<VAR>q : ℚ<VAR>n : ℕ<GOAL>q ^ n = Rat.divInt (q.num ^ n) (↑q.den ^ n)
<VAR>q : ℚ<VAR>n : ℕ<GOAL>(q ^ n).num = q.num ^ n
<VAR>q : ℚ<VAR>n : ℕ<GOAL>(q ^ n).den = q.den ^ n
<VAR>num : ℤ<VAR>den : ℕ<VAR>hd : den ≠ 0<VAR>hdn : num.natAbs.Coprime den<VAR>n : ℕ<GOAL>{ num := num, den := den, den_nz := hd, reduced := hdn } ^ n = { num := num ^ n, den := den ^ n, den_nz := ⋯, reduced := ⋯ }
<VAR>a b : ℤ<GOAL>(Rat.divInt a b)⁻¹ = Rat.divInt b a
<VAR>a : ℤ<VAR>b : ℕ<GOAL>(mkRat a b)⁻¹ = Rat.divInt (↑b) a
<VAR>q : ℚ<GOAL>q⁻¹ = Rat.divInt (↑q.den) q.num
<VAR>n₁ d₁ n₂ d₂ : ℤ<GOAL>Rat.divInt n₁ d₁ / Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂) (d₁ * n₂)
<VAR>q r : ℚ<GOAL>q / r = Rat.divInt (q.num * ↑r.den) (↑q.den * r.num)
<VAR>a : ℚ<GOAL>a + 0 = a
<VAR>a b : ℚ<GOAL>a + b = b + a
<VAR>a b c : ℚ<GOAL>a + b + c = a + (b + c)
<VAR>a : ℚ<GOAL>-a + a = 0
<VAR>n : ℤ<GOAL>Rat.divInt n 1 = ↑n
<VAR>n : ℤ<GOAL>mkRat n 1 = ↑n
<VAR>a b c : ℚ<GOAL>a * b * c = a * (b * c)
<VAR>a b c : ℚ<GOAL>(a + b) * c = a * c + b * c
<VAR>a b c : ℚ<GOAL>a * (b + c) = a * b + a * c
<VAR>a : ℚ<GOAL>a ≠ 0 → a * a⁻¹ = 1
<VAR>a : ℚ<VAR>h : a ≠ 0<GOAL>a⁻¹ * a = 1
<VAR>p q : ℚ<GOAL>p = q ↔ p.num * ↑q.den = q.num * ↑p.den
<VAR>q : ℚ<GOAL>(-q).den = q.den
<VAR>q : ℚ<GOAL>(-q).num = -q.num
<VAR>q : ℚ<VAR>hq : q.num = 0<GOAL>q = 0
<VAR>q : ℚ<GOAL>q = 0 ↔ q.num = 0
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hq : q ≠ 0<VAR>hqnd : q = Rat.divInt n d<GOAL>n ≠ 0
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hq : q ≠ 0<VAR>hqnd : q = Rat.divInt n d<GOAL>d ≠ 0
<VAR>n d : ℤ<VAR>h : n ≠ 0<VAR>hd : d ≠ 0<GOAL>Rat.divInt n d ≠ 0
<VAR>q : ℚ<GOAL>0 ≤ q → 0 ≤ -q → q = 0
<VAR>a : ℚ<GOAL>0 ≤ a ∨ 0 ≤ -a
<VAR>a b c : ℤ<GOAL>Rat.divInt (a + b) c = Rat.divInt a c + Rat.divInt b c
<VAR>n d : ℤ<GOAL>Rat.divInt n d = ↑n / ↑d
<VAR>n d : ℤ<GOAL>↑n / ↑d = Rat.divInt n d
<VAR>n d : ℕ<GOAL>↑n / ↑d = Rat.divInt ↑n ↑d
<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<GOAL>Rat.divInt n x * Rat.divInt x d = Rat.divInt n d
<VAR>q : ℚ<VAR>hq : q.den = 1<GOAL>↑q.num = q
<VAR>q : ℚ<VAR>h : q.isInt = true<GOAL>q = ↑q.num
<VAR>r : ℚ<GOAL>r.den = 1 ↔ ↑r.num = r
<VAR>m n : ℤ<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_3<VAR>DivisionSemiring α<GOAL>↑0 = 0
<VAR>α : Type u_3<VAR>DivisionSemiring α<GOAL>↑1 = 1
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q : ℚ≥0<VAR>a : α<GOAL>Commute (↑q) a
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>a : α<VAR>q : ℚ≥0<GOAL>Commute a ↑q
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q : ℚ≥0<VAR>a : α<GOAL>↑q * a = a * ↑q
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>a : ℕ<VAR>b : ℕ<VAR>hb : ↑b ≠ 0<GOAL>↑(NNRat.divNat a b) = ↑a / ↑b
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q + r) = ↑q + ↑r
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q * r) = ↑q * ↑r
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q : ℚ≥0<VAR>hq : ↑q.num ≠ 0<GOAL>↑q⁻¹ = (↑q)⁻¹
<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.num ≠ 0<GOAL>↑(q / r) = ↑q / ↑r
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_3<VAR>DivisionRing α<GOAL>↑0 = 0
<VAR>α : Type u_3<VAR>DivisionRing α<GOAL>↑1 = 1
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>r : ℚ<VAR>a : α<GOAL>Commute (↑r) a
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>r : ℚ<VAR>a : α<GOAL>↑r * a = a * ↑r
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>a : α<VAR>r : ℚ<GOAL>Commute a ↑r
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>a : ℤ<VAR>b : ℤ<VAR>b0 : ↑b ≠ 0<GOAL>↑(a /. b) = ↑a / ↑b
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : ↑b ≠ 0<GOAL>↑(mkRat a b) = ↑a / ↑b
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>q r : ℚ<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q + r) = ↑q + ↑r
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>q : ℚ<GOAL>↑(-q) = -↑q
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p - q) = ↑p - ↑q
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p * q) = ↑p * ↑q
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>q : ℚ<VAR>hq : ↑q.num ≠ 0<GOAL>↑q⁻¹ = (↑q)⁻¹
<VAR>α : Type u_3<VAR>DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.num ≠ 0<GOAL>↑(p / q) = ↑p / ↑q
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>DivisionSemiring α<VAR>DivisionSemiring β<VAR>RingHomClass F α β<VAR>f : F<VAR>q : ℚ≥0<GOAL>f ↑q = ↑q
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>DivisionSemiring α<VAR>FunLike F ℚ≥0 α<VAR>RingHomClass F ℚ≥0 α<VAR>f : F<VAR>q : ℚ≥0<GOAL>f q = ↑q
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>FunLike F α β<VAR>DivisionRing α<VAR>DivisionRing β<VAR>RingHomClass F α β<VAR>f : F<VAR>q : ℚ<GOAL>f ↑q = ↑q
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>DivisionRing α<VAR>FunLike F ℚ α<VAR>RingHomClass F ℚ α<VAR>f : F<VAR>q : ℚ<GOAL>f q = ↑q
<VAR>F : Type u_1<VAR>M₀ : Type u_5<VAR>MonoidWithZero M₀<VAR>FunLike F ℚ M₀<VAR>MonoidWithZeroHomClass F ℚ M₀<VAR>f g : F<VAR>h : ∀ (m : ℤ), f ↑m = g ↑m<GOAL>f = g
<VAR>M₀ : Type u_5<VAR>MonoidWithZero M₀<VAR>f g : ℚ →*₀ M₀<VAR>h : f.comp ↑(Int.castRingHom ℚ) = g.comp ↑(Int.castRingHom ℚ)<GOAL>f = g
<VAR>F : Type u_1<VAR>M₀ : Type u_5<VAR>MonoidWithZero M₀<VAR>FunLike F ℚ M₀<VAR>MonoidWithZeroHomClass F ℚ M₀<VAR>f g : F<VAR>same_on_neg_one : f (-1) = g (-1)<VAR>same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n<GOAL>f = g
<VAR>F : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>FunLike F ℚ R<VAR>RingHomClass F ℚ R<VAR>f g : F<GOAL>f = g
<VAR>α : Type u_13<VAR>M : Type u_14<VAR>Zero M<VAR>self : α →₀ M<VAR>a : α<GOAL>a ∈ self.support ↔ self.toFun a ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f g : α →₀ M<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f g : α →₀ M<GOAL>f ≠ g ↔ ∃ a, f a ≠ g a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>s : Finset α<VAR>h : ∀ (a : α), a ∈ s ↔ f a ≠ 0<GOAL>⇑{ support := s, toFun := f, mem_support_toFun := h } = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>⇑0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<GOAL>0 a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<GOAL>Finsupp.support 0 = ∅
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>a ∈ f.support ↔ f a ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>Function.support ⇑f = ↑f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>a ∉ f.support ↔ f a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>⇑f = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f g : α →₀ M<GOAL>f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.support = ∅ ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.support.Nonempty ↔ f ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.support.card = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>(Function.support ⇑f).Finite
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>s : Set α<VAR>f : α →₀ M<GOAL>↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Finite α<VAR>f : α → M<GOAL>(Finsupp.equivFunOnFinite.symm f).support = ⋯.toFinset
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Finite α<GOAL>∀ (a : α →₀ M) (a_1 : α), Finsupp.equivFunOnFinite a a_1 = a a_1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Finite α<VAR>f : α → M<GOAL>∀ (a : α), (Finsupp.equivFunOnFinite.symm f) a = f a
<VAR>M : Type u_5<VAR>Zero M<VAR>α : Type u_13<VAR>Finite α<VAR>f : α →₀ M<GOAL>Finsupp.equivFunOnFinite.symm ⇑f = f
<VAR>M : Type u_5<VAR>Zero M<VAR>ι : Type u_13<VAR>Unique ι<GOAL>∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default
<VAR>M : Type u_5<VAR>Zero M<VAR>ι : Type u_13<VAR>Unique ι<GOAL>∀ (a : M), (Equiv.finsuppUnique.symm a).support.val = Multiset.map Subtype.val Finset.univ.val
<VAR>M : Type u_5<VAR>Zero M<VAR>ι : Type u_13<VAR>Unique ι<GOAL>∀ (a : M) (a_1 : ι), (Equiv.finsuppUnique.symm a) a_1 = a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Unique α<VAR>f g : α →₀ M<VAR>h : f default = g default<GOAL>f = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Unique α<VAR>f g : α →₀ M<GOAL>f = g ↔ f default = g default
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<VAR>Decidable (a = a')<GOAL>(Finsupp.single a b) a' = if a = a' then b else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x z : α<VAR>y : M<GOAL>(Finsupp.single (f x) y) (f z) = (Finsupp.single x y) z
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>⇑(Finsupp.single a b) = {a}.indicator fun x => b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>(Finsupp.single a b) a = b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<VAR>h : a ≠ a'<GOAL>(Finsupp.single a b) a' = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>a : α<VAR>b : M<GOAL>⇑(Finsupp.single a b) = Function.update 0 a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>a : α<VAR>b : M<GOAL>⇑(Finsupp.single a b) = Pi.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<GOAL>Finsupp.single a 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<GOAL>Finsupp.single a ((Finsupp.single a' b) a) = (Finsupp.single a' (Finsupp.single a' b)) a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>b : M<VAR>a : α<VAR>hb : b ≠ 0<GOAL>(Finsupp.single a b).support = {a}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>(Finsupp.single a b).support ⊆ {a}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<VAR>x : α<GOAL>(Finsupp.single a b) x ∈ {0, b}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>Set.range ⇑(Finsupp.single a b) ⊆ {0, b}
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<GOAL>Function.Injective (Finsupp.single a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a x : α<VAR>b : M<GOAL>(Finsupp.single a b) x = 0 ↔ x = a → b = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a x : α<VAR>b : M<GOAL>(Finsupp.single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<GOAL>a ∈ (Finsupp.single a' b).support ↔ a = a' ∧ b ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>f = Finsupp.single a b ↔ f.support ⊆ {a} ∧ f a = b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a₁ a₂ : α<VAR>b₁ b₂ : M<GOAL>Finsupp.single a₁ b₁ = Finsupp.single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>b : M<VAR>h : b ≠ 0<GOAL>Function.Injective fun a => Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<VAR>h : b ≠ 0<GOAL>Finsupp.single a b = Finsupp.single a' b ↔ a = a'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>b : M<VAR>i : α<VAR>h : b ≠ 0<GOAL>(Finsupp.single i b).support ≠ ⊥
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>b b' : M<VAR>hb : b ≠ 0<VAR>hb' : b' ≠ 0<VAR>i j : α<GOAL>Disjoint (Finsupp.single i b).support (Finsupp.single j b').support ↔ i ≠ j
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>Finsupp.single a b = 0 ↔ b = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a₁ a₂ : α<VAR>b : M<GOAL>(Finsupp.single a₁ b) a₂ = (Finsupp.single a₂ b) a₁
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Unique α<VAR>x : α →₀ M<GOAL>x = Finsupp.single default (x default)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<VAR>Unique α<VAR>b' : M<GOAL>Finsupp.single a b = Finsupp.single a' b' ↔ b = b'
<VAR>α : Type u_1<VAR>N : Type u_7<VAR>P : Type u_8<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>F : Type u_13<VAR>FunLike F N P<VAR>AddMonoidHomClass F N P<VAR>e : F<VAR>a : α<VAR>n : N<VAR>b : α<GOAL>e ((Finsupp.single a n) b) = (Finsupp.single a (e n)) b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>f.support = {a} ↔ f a ≠ 0 ∧ f = Finsupp.single a (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>f.support = {a} ↔ ∃ b, b ≠ 0 ∧ f = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.support.card = 1 ↔ ∃ a, f a ≠ 0 ∧ f = Finsupp.single a (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<GOAL>f.support.card = 1 ↔ ∃ a b, b ≠ 0 ∧ f = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>f.support ⊆ {a} ↔ f = Finsupp.single a (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>f.support ⊆ {a} ↔ ∃ b, f = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Nonempty α<VAR>f : α →₀ M<GOAL>f.support.card ≤ 1 ↔ ∃ a, f = Finsupp.single a (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>Nonempty α<VAR>f : α →₀ M<GOAL>f.support.card ≤ 1 ↔ ∃ a b, f = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>Finite α<VAR>x : α<VAR>m : M<GOAL>Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>Finite α<VAR>x : α<VAR>m : M<GOAL>Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>DecidableEq α<GOAL>⇑(f.update a b) = Function.update (⇑f) a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>f.update a (f a) = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>Finsupp.update 0 a b = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>DecidableEq α<VAR>DecidableEq M<GOAL>(f.update a b).support = if b = 0 then f.support.erase a else insert a f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>DecidableEq α<GOAL>(f.update a 0).support = f.support.erase a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>DecidableEq α<VAR>h : b ≠ 0<GOAL>(f.update a b).support = insert a f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>DecidableEq α<VAR>DecidableEq M<GOAL>(f.update a b).support ⊆ insert a f.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a₁ a₂ : α<VAR>h : a₁ ≠ a₂<VAR>m₁ m₂ : M<GOAL>(f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b c : M<GOAL>(f.update a b).update a c = f.update a c
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>a : α<VAR>f : α →₀ M<GOAL>(Finsupp.erase a f).support = f.support.erase a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>f : α →₀ M<GOAL>(Finsupp.erase a f) a = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>f : α →₀ M<VAR>h : a' ≠ a<GOAL>(Finsupp.erase a f) a' = f a'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq α<VAR>a a' : α<VAR>f : α →₀ M<GOAL>(Finsupp.erase a f) a' = if a' = a then 0 else f a'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<VAR>b : M<GOAL>Finsupp.erase a (Finsupp.single a b) = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a a' : α<VAR>b : M<VAR>h : a ≠ a'<GOAL>Finsupp.erase a (Finsupp.single a' b) = Finsupp.single a' b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>haf : a ∉ f.support<GOAL>Finsupp.erase a f = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>a : α<GOAL>Finsupp.erase a 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>Finsupp.erase a f = f.update a 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a a' : α<VAR>ha : a ≠ a'<VAR>b : M<GOAL>Finsupp.erase a (f.update a' b) = (Finsupp.erase a f).update a' b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>Finsupp.erase a (Finsupp.erase a f) = Finsupp.erase a f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>(Finsupp.erase a f).update a b = f.update a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>Finsupp.erase a (f.update a b) = Finsupp.erase a f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<GOAL>⇑(Finsupp.onFinset s f hf) = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<VAR>a : α<GOAL>(Finsupp.onFinset s f hf) a = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<GOAL>(Finsupp.onFinset s f hf).support ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<VAR>a : α<GOAL>a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>DecidableEq M<VAR>s : Finset α<VAR>f : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<GOAL>(Finsupp.onFinset s f hf).support = Finset.filter (fun a => f a ≠ 0) s
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>f : α → M<VAR>hf : (Function.support f).Finite<GOAL>⇑(Finsupp.ofSupportFinite f hf) = f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>g : α →₀ M<VAR>a : α<GOAL>(Finsupp.mapRange f hf g) a = f (g a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M → N<VAR>hf : f 0 = 0<GOAL>Finsupp.mapRange f hf 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>Zero M<VAR>g : α →₀ M<GOAL>Finsupp.mapRange id ⋯ g = g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : N → P<VAR>hf : f 0 = 0<VAR>f₂ : M → N<VAR>hf₂ : f₂ 0 = 0<VAR>h : (f ∘ f₂) 0 = 0<VAR>g : α →₀ M<GOAL>Finsupp.mapRange (f ∘ f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange f hf g).support ⊆ g.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>a : α<VAR>b : M<GOAL>Finsupp.mapRange f hf (Finsupp.single a b) = Finsupp.single a (f b)
<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>e : M → N<VAR>he0 : e 0 = 0<VAR>f : ι →₀ M<VAR>he : Function.Injective e<GOAL>(Finsupp.mapRange e he0 f).support = f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>v : α →₀ M<GOAL>(Finsupp.embDomain f v).support = Finset.map f v.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<GOAL>Finsupp.embDomain f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>v : α →₀ M<VAR>a : α<GOAL>(Finsupp.embDomain f v) (f a) = v a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>v : α →₀ M<VAR>a : β<VAR>h : a ∉ Set.range ⇑f<GOAL>(Finsupp.embDomain f v) a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<GOAL>Function.Injective (Finsupp.embDomain f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>l₁ l₂ : α →₀ M<GOAL>Finsupp.embDomain f l₁ = Finsupp.embDomain f l₂ ↔ l₁ = l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>l : α →₀ M<GOAL>Finsupp.embDomain f l = 0 ↔ l = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>N : Type u_7<VAR>Zero M<VAR>Zero N<VAR>f : α ↪ β<VAR>g : M → N<VAR>p : α →₀ M<VAR>hg : g 0 = 0<GOAL>Finsupp.embDomain f (Finsupp.mapRange g hg p) = Finsupp.mapRange g hg (Finsupp.embDomain f p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>l : α →₀ M<VAR>f : α ↪ β<VAR>a : β<VAR>b : M<VAR>hb : b ≠ 0<VAR>h : Finsupp.embDomain f l = Finsupp.single a b<GOAL>∃ x, l = Finsupp.single x b ∧ f x = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>Zero M<VAR>f : α ↪ β<VAR>a : α<VAR>m : M<GOAL>Finsupp.embDomain f (Finsupp.single a m) = Finsupp.single (f a) m
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>g₁ : α →₀ M<VAR>g₂ : α →₀ N<VAR>a : α<GOAL>(Finsupp.zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>D : DecidableEq α<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>g₁ : α →₀ M<VAR>g₂ : α →₀ N<GOAL>(Finsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Zero M<VAR>Zero N<VAR>Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>a : α<VAR>m : M<VAR>n : N<GOAL>Finsupp.zipWith f hf (Finsupp.single a m) (Finsupp.single a n) = Finsupp.single a (f m n)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f g : α →₀ M<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>g₁ g₂ : α →₀ M<VAR>a : α<GOAL>(g₁ + g₂) a = g₁ a + g₂ a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>DecidableEq α<VAR>g₁ g₂ : α →₀ M<GOAL>(g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<GOAL>(g₁ + g₂).support = g₁.support ∪ g₂.support
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>b₁ b₂ : M<GOAL>Finsupp.single a (b₁ + b₂) = Finsupp.single a b₁ + Finsupp.single a b₂
<VAR>M : Type u_13<VAR>AddZeroClass M<VAR>d : M<GOAL>AddEquiv.finsuppUnique.symm d = Finsupp.single () d
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>b : M<GOAL>(Finsupp.singleAddHom a) b = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>a : α<VAR>g : α →₀ M<GOAL>(Finsupp.applyAddHom a) g = g a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<GOAL>∀ (a : α →₀ M) (a_1 : α), Finsupp.coeFnAddHom a a_1 = a a_1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>f.update a b = Finsupp.single a b + Finsupp.erase a f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddZeroClass M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>f.update a b = Finsupp.erase a f + Finsupp.single a b