internlm/Lean-Github huggingface dataset:
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h2 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
c k a : ℕ
h : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
⊢ f
      (⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.snd,
        n - ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.snd) =
    f
      (((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.snd, ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).snd,
        ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.snd,
        n - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h).snd)
Tactic:
simp only [mem_sigma, mem_range, Nat.lt_succ_iff] at h
Proof state after:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h2 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ f
      (⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.snd,
        n - ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.snd) =
    f
      (((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.snd, ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).snd,
        ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.snd,
        n - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).snd)
Theorem: Finset.sum_4_rw
Proof state before:
case mk.mk
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ × ℕ × ℕ × ℕ → α
n : ℕ
φ : (_ : (_ : ℕ) × ℕ) × ℕ → (_ : (_ : ℕ) × ℕ) × ℕ :=
  fun x =>
    match x with
    | ⟨⟨k, a⟩, c⟩ => ⟨⟨a + c, a⟩, k - a⟩
h1 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun l => range (l + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h2 :
  ∀ (a : (_ : (_ : ℕ) × ℕ) × ℕ)
    (ha : a ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)),
    (fun m x => φ m) ((fun m x => φ m) a ha)
        ((fun m x => φ m) a ha ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)) =
      a
c k a : ℕ
h✝ : ⟨⟨k, a⟩, c⟩ ∈ ((range (n + 1)).sigma fun k => range (k + 1)).sigma fun x => range (n - x.fst + 1)
h : (k ≤ n ∧ a ≤ k) ∧ c ≤ n - k
⊢ f
      (⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.fst.snd, ⟨⟨k, a⟩, c⟩.snd,
        n - ⟨⟨k, a⟩, c⟩.fst.fst - ⟨⟨k, a⟩, c⟩.snd) =
    f
      (((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.snd, ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).snd,
        ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.snd,
        n - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).fst.fst - ((fun m x => φ m) ⟨⟨k, a⟩, c⟩ h✝).snd)
Tactic:
simp only [Nat.add_sub_self_left a c, Nat.sub_sub,
  add_comm (a + c), ← add_assoc, Nat.sub_add_cancel h.1.2]
Proof state after:
no goals
Theorem: range_sym_prop
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = m
Tactic:
simp only [Finset.mem_sym_iff] at hk
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = m
Theorem: range_sym_prop
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = m
Tactic:
simp_rw [← k.prop]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = Multiset.card ↑k
Theorem: range_sym_prop
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = Multiset.card ↑k
Tactic:
rw [← Multiset.toFinset_sum_count_eq]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k
Theorem: range_sym_prop
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k
Tactic:
apply symm
Proof state after:
case a
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k = ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k
Theorem: range_sym_prop
Proof state before:
case a
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k = ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k
Tactic:
apply Finset.sum_subset_zero_on_sdiff
Proof state after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ (↑k).toFinset ⊆ Finset.range (n + 1)

case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ Finset.range (n + 1) \ (↑k).toFinset, Multiset.count x ↑k = 0

case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ (↑k).toFinset, Multiset.count x ↑k = Multiset.count x ↑k
Theorem: range_sym_prop
Proof state before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ (↑k).toFinset ⊆ Finset.range (n + 1)
Tactic:
intro i hi
Proof state after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ (↑k).toFinset
⊢ i ∈ Finset.range (n + 1)
Theorem: range_sym_prop
Proof state before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ (↑k).toFinset
⊢ i ∈ Finset.range (n + 1)
Tactic:
simp only [Sym.val_eq_coe, Multiset.mem_toFinset, Sym.mem_coe] at hi
Proof state after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ k
⊢ i ∈ Finset.range (n + 1)
Theorem: range_sym_prop
Proof state before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ k
⊢ i ∈ Finset.range (n + 1)
Tactic:
exact hk i hi
Proof state after:
no goals
Theorem: range_sym_prop
Proof state before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ Finset.range (n + 1) \ (↑k).toFinset, Multiset.count x ↑k = 0
Tactic:
intro x hx
Proof state after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x ∈ Finset.range (n + 1) \ (↑k).toFinset
⊢ Multiset.count x ↑k = 0
Theorem: range_sym_prop
Proof state before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x ∈ Finset.range (n + 1) \ (↑k).toFinset
⊢ Multiset.count x ↑k = 0
Tactic:
simp only [Sym.val_eq_coe, Finset.mem_sdiff, Finset.mem_range, Multiset.mem_toFinset, Sym.mem_coe] at hx
Proof state after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ Multiset.count x ↑k = 0
Theorem: range_sym_prop
Proof state before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ Multiset.count x ↑k = 0
Tactic:
simp only [Multiset.count_eq_zero, Sym.mem_coe]
Proof state after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ x ∉ k
Theorem: range_sym_prop
Proof state before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ x ∉ k
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: range_sym_prop
Proof state before:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ (↑k).toFinset, Multiset.count x ↑k = Multiset.count x ↑k
Tactic:
intro x _
Proof state after:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
a✝ : x ∈ (↑k).toFinset
⊢ Multiset.count x ↑k = Multiset.count x ↑k
Theorem: range_sym_prop
Proof state before:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
a✝ : x ∈ (↑k).toFinset
⊢ Multiset.count x ↑k = Multiset.count x ↑k
Tactic:
rfl
Proof state after:
no goals
Theorem: range_sym_weighted_sum_le
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ m * n
Tactic:
suffices h : ∀ i ∈ Finset.range (n + 1), Multiset.count i k * i ≤ Multiset.count i k * n by
  apply le_trans (Finset.sum_le_sum h)
  rw [← Finset.sum_mul, range_sym_prop hk]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
Theorem: range_sym_weighted_sum_le
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
Tactic:
intro i hi
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
Theorem: range_sym_weighted_sum_le
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
Tactic:
apply Nat.mul_le_mul_left
Proof state after:
case h
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n
Theorem: range_sym_weighted_sum_le
Proof state before:
case h
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n
Tactic:
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
Proof state after:
no goals
Theorem: range_sym_weighted_sum_le
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h : ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ m * n
Tactic:
apply le_trans (Finset.sum_le_sum h)
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h : ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * n ≤ m * n
Theorem: range_sym_weighted_sum_le
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h : ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * n ≤ m * n
Tactic:
rw [← Finset.sum_mul, range_sym_prop hk]
Proof state after:
no goals
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) =
    m * n - ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i
Tactic:
suffices h : (((Finset.range (n + 1)).sum fun i => Multiset.count i k * (n - i)) +
      (Finset.range (n + 1)).sum fun i => Multiset.count i k * i) = m * n by
  rw [← h, Nat.add_sub_cancel]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n
Tactic:
rw [← Finset.sum_add_distrib]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), (Multiset.count x ↑k * (n - x) + Multiset.count x ↑k * x) = m * n
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), (Multiset.count x ↑k * (n - x) + Multiset.count x ↑k * x) = m * n
Tactic:
simp_rw [← mul_add]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Tactic:
have :
  ∀ x ∈ Finset.range (n + 1),
    Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n := by
  intro x hx
  rw [Nat.sub_add_cancel (Nat.lt_succ_iff.mp (Finset.mem_range.mp hx))]
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
this : ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
this : ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Tactic:
rw [Finset.sum_congr rfl this, ← Finset.sum_mul, range_sym_prop hk]
Proof state after:
no goals
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h :
  ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) =
    m * n - ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i
Tactic:
rw [← h, Nat.add_sub_cancel]
Proof state after:
no goals
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
Tactic:
intro x hx
Proof state after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
Theorem: sum_range_sym_mul_compl
Proof state before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
Tactic:
rw [Nat.sub_add_cancel (Nat.lt_succ_iff.mp (Finset.mem_range.mp hx))]
Proof state after:
no goals
Theorem: MonoidAlgebra.algHom_apply_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : DecidableEq α
inst✝⁵ : Semiring N
inst✝⁴ : Semiring P
inst✝³ : Monoid α
inst✝² : CommSemiring R
inst✝¹ : Algebra R N
inst✝ : Algebra R P
e : N →ₐ[R] P
x : MonoidAlgebra N α
a : α
⊢ ((algHom e) x) a = e (x a)
Tactic:
simp [algHom]
Proof state after:
no goals
Theorem: MonoidAlgebra.algHom_apply_single
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : DecidableEq α
inst✝⁵ : Semiring N
inst✝⁴ : Semiring P
inst✝³ : Monoid α
inst✝² : CommSemiring R
inst✝¹ : Algebra R N
inst✝ : Algebra R P
e : N →ₐ[R] P
a : α
n : N
⊢ (algHom e) (single a n) = single a (e n)
Tactic:
simp [algHom]
Proof state after:
no goals
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = x a ⊗ₜ[R] n
Tactic:
simp only [rTensorAlgHom]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((Algebra.TensorProduct.lift (algHom Algebra.TensorProduct.includeLeft)
          (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) ⋯)
        (x ⊗ₜ[R] n))
      a =
    x a ⊗ₜ[R] n
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((Algebra.TensorProduct.lift (algHom Algebra.TensorProduct.includeLeft)
          (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) ⋯)
        (x ⊗ₜ[R] n))
      a =
    x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.lift_tmul]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x * (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) n) a =
    x a ⊗ₜ[R] n
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x * (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) n) a =
    x a ⊗ₜ[R] n
Tactic:
rw [AlgHom.comp_apply, singleOneAlgHom_apply, mul_single_one_apply]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * Algebra.TensorProduct.includeRight n = x a ⊗ₜ[R] n
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * Algebra.TensorProduct.includeRight n = x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.includeRight_apply]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Tactic:
simp only [algHom_apply_apply, Algebra.TensorProduct.includeLeft_apply]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ x a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ x a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
Proof state after:
no goals
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft' R M N α S)
Tactic:
ext x n
Proof state after:
case a.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ ((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap) x) n =
    ((AlgebraTensorModule.curry ↑(finsuppLeft' R M N α S)) x) n
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ ((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap) x) n =
    ((AlgebraTensorModule.curry ↑(finsuppLeft' R M N α S)) x) n
Tactic:
dsimp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
Proof state after:
case a.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ rTensorAlgHom (x ⊗ₜ[R] n) = ↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)