case h
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ↑(1 • b) x = ↑b x
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
⊢ 1 • b = b
ext x
case h
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
case h
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ↑(1 • b) x = ↑b x
rw [smul_apply]
case pos
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x

case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
case h
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
by_cases x0 : x = 0
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in {(1, x)}, ↑1 x.fst • ↑b x.snd = ↑b x

case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∀ (x_1 : ℕ × ℕ), x_1 ∈ divisorsAntidiagonal x → ¬x_1 ∈ {(1, x)} → ↑1 x_1.fst • ↑b x_1.snd = 0
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
rw [← sum_subset h]
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
⊢ ↑1 y.fst • ↑b y.snd = 0
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∀ (x_1 : ℕ × ℕ), x_1 ∈ divisorsAntidiagonal x → ¬x_1 ∈ {(1, x)} → ↑1 x_1.fst • ↑b x_1.snd = 0
intro y ymem ynmem
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
y1ne : y.fst ≠ 1
⊢ ↑1 y.fst • ↑b y.snd = 0
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
⊢ ↑1 y.fst • ↑b y.snd = 0
have y1ne : y.fst ≠ 1 := by
  intro con
  simp only [Con, mem_divisorsAntidiagonal, one_mul, Ne.def] at ymem
  simp only [mem_singleton, Prod.ext_iff] at ynmem
  cases y
  subst con
  simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem
  tauto
no goals
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
y1ne : y.fst ≠ 1
⊢ ↑1 y.fst • ↑b y.snd = 0
simp [y1ne]
no goals
case pos
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
simp [x0]
no goals
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ {(1, x)} ⊆ divisorsAntidiagonal x
simp [x0]
no goals
case neg
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in {(1, x)}, ↑1 x.fst • ↑b x.snd = ↑b x
simp
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
⊢ False
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
⊢ y.fst ≠ 1
intro con
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
⊢ False
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
⊢ False
simp only [Con, mem_divisorsAntidiagonal, one_mul, Ne.def] at ymem
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
ynmem : ¬(y.fst = 1 ∧ y.snd = x)
⊢ False
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
⊢ False
simp only [mem_singleton, Prod.ext_iff] at ynmem
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
fst✝ snd✝ : ℕ
con : (fst✝, snd✝).fst = 1
ymem : (fst✝, snd✝).fst * (fst✝, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((fst✝, snd✝).fst = 1 ∧ (fst✝, snd✝).snd = x)
⊢ False
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
ynmem : ¬(y.fst = 1 ∧ y.snd = x)
⊢ False
cases y
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ymem : (1, snd✝).fst * (1, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((1, snd✝).fst = 1 ∧ (1, snd✝).snd = x)
⊢ False
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
fst✝ snd✝ : ℕ
con : (fst✝, snd✝).fst = 1
ymem : (fst✝, snd✝).fst * (fst✝, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((fst✝, snd✝).fst = 1 ∧ (fst✝, snd✝).snd = x)
⊢ False
subst con
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ynmem : ¬snd✝ = x
ymem : snd✝ = x
⊢ False
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ymem : (1, snd✝).fst * (1, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((1, snd✝).fst = 1 ∧ (1, snd✝).snd = x)
⊢ False
simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem
no goals
case mk
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ynmem : ¬snd✝ = x
ymem : snd✝ = x
⊢ False
tauto